projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ef7b7bb) | patch
Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions.
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 29 Sep 2015 13:17:03 +0000 (15:17 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 29 Sep 2015 13:17:03 +0000 (15:17 +0200)
commit4182943e7accc8a0e05f6dfdf9db7db06e94c6cd
treed4f3bad70e464321a4e7fe977f1528f783dcd1b1tree
parentef7b7bba7bc9b207d5a2198518f21b13490caa32commit | diff
Fix for fmf+incremental. Restrict cbqi to literals from ce body.  Add regressions.
13 files changed:
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/quant_conflict_find.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/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history
test/regress/regress0/push-pop/Makefile.am diff | blob | history
test/regress/regress0/push-pop/fmf-fun-dbu.smt2 [new file with mode: 0644] blob
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/clock-inc-tuple.sy [new file with mode: 0644] blob