projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1d29f56) | patch
Add lazy strategy for bounded integers to avoid non-terminating unsat cases. Add...
authorajreynol <reynolds@larapc05.epfl.ch>
Tue, 13 May 2014 15:18:18 +0000 (17:18 +0200)
committerajreynol <reynolds@larapc05.epfl.ch>
Tue, 13 May 2014 15:18:23 +0000 (17:18 +0200)
commit977bdcdcbab6ffdf757e3837d2f555a53cbb6daf
treeb32a630f5c780ec77ba2ffbce0f498252de7d7b1tree
parent1d29f568aba39501d09284c4139847fbe688efcccommit | diff
Add lazy strategy for bounded integers to avoid non-terminating unsat cases.  Add regressions.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/bi-artm-s.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/artemis-0512-nonterm.smt2 [new file with mode: 0644] blob