projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ace360b) | patch
Fix bug related to quantifiers + incremental, thanks John Backes for the bug report...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 15 Sep 2015 08:39:29 +0000 (10:39 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 15 Sep 2015 08:39:29 +0000 (10:39 +0200)
commitbad7f4fe4dca4c6511c2862bf81b6791640ac78f
tree0be31a9300766d39ae36c9efba02e2c5a68dd156tree
parentace360b4da1edef06088a366dc21b58f9431efc2commit | diff
Fix bug related to quantifiers + incremental, thanks John Backes for the bug report.  Other minor cleanup.
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
test/regress/regress0/push-pop/Makefile.am diff | blob | history
test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 [new file with mode: 0644] blob