projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fd07620) | patch
Add regressions for finite model finding
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 22 May 2013 21:33:15 +0000 (16:33 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 22 May 2013 21:33:30 +0000 (16:33 -0500)
commit852d41b2878ae4981ab4a9b246345bb05bbe23ab
tree8f19be94ed3432517a3dcde87c6bb6eb868203f0tree
parentfd076209b073aff3ad3db6eccfc51a59ec5d87c2commit | diff
Add regressions for finite model finding
14 files changed:
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/fmf/ALG008-1.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt [new file with mode: 0644] blob
test/regress/regress0/fmf/Hoare-z3.931718.smt [new file with mode: 0644] blob
test/regress/regress0/fmf/Makefile.am [new file with mode: 0755] blob
test/regress/regress0/fmf/PUZ001+1.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/QEpres-uf.855035.smt [new file with mode: 0644] blob
test/regress/regress0/fmf/agree466.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/agree467.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/german169.smt2 [new file with mode: 0755] blob
test/regress/regress0/fmf/german73.smt2 [new file with mode: 0755] blob
test/regress/regress0/fmf/refcount24.cvc.smt2 [new file with mode: 0755] blob