projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2f282e6) | patch
Fixed bug in bv rewriter that caused wrong answer in SMT-COMP
authorClark Barrett <barrett@cs.nyu.edu>
Thu, 28 Jun 2012 11:26:07 +0000 (11:26 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Thu, 28 Jun 2012 11:26:07 +0000 (11:26 +0000)
commit7fcf0cb48a02115ff93395b89db722d10abf5f41
treec087609c08ac23331122470afc037a6da463b7c5tree
parent2f282e67ed10bd58c24cdc14ec53857b79e59a35commit | diff
Fixed bug in bv rewriter that caused wrong answer in SMT-COMP
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_simplification.h diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history
test/regress/regress0/aufbv/rewrite_bug.smt [new file with mode: 0644] blob
test/regress/regress0/bv/Makefile.am diff | blob | history
test/regress/regress0/bv/smtcompbug.smt [new file with mode: 0644] blob