projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fbbd4e9) | patch
Fix to term normalization of integer equalities. Adds a regression test that triggere...
authorTim King <taking@cs.nyu.edu>
Mon, 11 Jun 2012 23:40:47 +0000 (23:40 +0000)
committerTim King <taking@cs.nyu.edu>
Mon, 11 Jun 2012 23:40:47 +0000 (23:40 +0000)
commitcdb023736199d99d8202f248793cd465bfdae4fb
tree4cb426e78d6098cc54f723c528a1e62be55598bdtree
parentfbbd4e966395aa3c8094ef137aa17be5f372e2b0commit | diff
Fix to term normalization of integer equalities. Adds a regression test that triggered it.
src/theory/arith/normal_form.cpp diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/regress0/uflia/Makefile.am diff | blob | history
test/regress/regress0/uflia/error30.smt [new file with mode: 0644] blob