projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e85f690) | patch
Partial fix in arithmetic for propagating shared terms. This partially resolves bug...
authorTim King <taking@cs.nyu.edu>
Thu, 15 Dec 2011 20:39:20 +0000 (20:39 +0000)
committerTim King <taking@cs.nyu.edu>
Thu, 15 Dec 2011 20:39:20 +0000 (20:39 +0000)
commit9bcda83d2d322a97b5896ce160c298f6a159a2d2
tree0004a4ad7f84c996230ad168a9ca73c20018a374tree
parente85f690a704a4182a8ffc8b96cff71737f5c0904commit | diff
Partial fix in arithmetic for propagating shared terms. This partially resolves bug 289.  Adds failing tests to regress1.
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/regress1/Makefile.am diff | blob | history
test/regress/regress1/hash_sat_06_19.smt2 [new file with mode: 0644] blob
test/regress/regress1/hash_sat_07_17.smt2 [new file with mode: 0644] blob
test/regress/regress1/hash_sat_09_09.smt2 [new file with mode: 0644] blob
test/regress/regress1/hash_sat_10_09.smt2 [new file with mode: 0644] blob
test/regress/regress1/ooo.tag10.smt2 [new file with mode: 0644] blob
test/regress/regress1/xs-11-20-5-2-5-3.smt2 [new file with mode: 0644] blob