projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 44ac537) | patch
Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for divisi...
authorTim King <taking@cs.nyu.edu>
Thu, 8 Nov 2012 23:54:18 +0000 (23:54 +0000)
committerTim King <taking@cs.nyu.edu>
Thu, 8 Nov 2012 23:54:18 +0000 (23:54 +0000)
commit2979089be3bc655d8bdd6245e193f356b4f7c93c
treeddb51fd7df95a39e7c67c3c08a3c6cbd3cc9ff42tree
parent44ac537312dcba8fc179f5ea9489e8cd7266f71ccommit | diff
Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for division by 0.
13 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/regress0/arith/Makefile.am diff | blob | history
test/regress/regress0/arith/div.01.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/div.02.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/div.03.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/div.04.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/div.05.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/div.06.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/div.07.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/div.08.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/mod.02.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/mod.03.smt2 [new file with mode: 0644] blob