projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8c325a4) | patch
Improved error reporting for improperly using non-linear division in linear arithmetic.
authorTim King <taking@cs.nyu.edu>
Mon, 12 Nov 2012 23:50:29 +0000 (23:50 +0000)
committerTim King <taking@cs.nyu.edu>
Mon, 12 Nov 2012 23:50:29 +0000 (23:50 +0000)
commit79b80442e5df070fe838de3fe4c09b235f6bddf5
tree7aed459a84a1ab94b7a6e90f2d308cd24488430btree
parent8c325a4bf6888e33fb8fdc1e071a8aab4aa20b6fcommit | diff
Improved error reporting for improperly using non-linear division in linear arithmetic.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/normal_form.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.09.smt2 [new file with mode: 0644] blob