projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 63df35c) | patch
Do not regress explanations of datatype lemmas (#5376)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 9 Nov 2020 13:42:03 +0000 (07:42 -0600)
committerGitHub <noreply@github.com>
Mon, 9 Nov 2020 13:42:03 +0000 (07:42 -0600)
commit6cb2e5743bd886115124256c2a3ad689a5b822a2
tree9376134244e1fc6729bc10a1a78fcdf2ee73d76dtree
parent63df35c477ee9e6c7bdeae677656dd374563de55commit | diff
Do not regress explanations of datatype lemmas (#5376)

This modifies datatypes to not regress explanations for lemmas. This avoids segfaults in some corner cases of sygus (see attached) and leads to slightly better performance on Facebook verification benchmarks.
src/theory/datatypes/inference_manager.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress2/sygus/policyM.sy [new file with mode: 0644] blob