projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b18ebfd) | patch
Always flush lemmas from downwards closure in sets (#4297)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Apr 2020 05:52:33 +0000 (00:52 -0500)
committerGitHub <noreply@github.com>
Wed, 15 Apr 2020 05:52:33 +0000 (00:52 -0500)
commit617f1b0fe93e077d6e76e03dcf1a75730740fe27
treef90a752936d1d3c218bc52517af53f4e7e19cae6tree
parentb18ebfd50bfcb3b2ec422daf5b2fd8d99ca6406acommit | diff
Always flush lemmas from downwards closure in sets (#4297)

Fixes #4283.

This also makes a few minor improvements to how lemmas are sent in sets. In particular, lemmas are not sent if we are already in conflict.
src/theory/sets/inference_manager.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history