projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 994e6eb) | patch
Fix for iff terms over equalities between the same term and differing constants.
authorTim King <taking@cs.nyu.edu>
Mon, 1 Apr 2013 19:39:25 +0000 (15:39 -0400)
committerTim King <taking@cs.nyu.edu>
Mon, 1 Apr 2013 19:53:01 +0000 (15:53 -0400)
commitcba10a096d97e82bd112b4d99a6ebe399d1369d6
tree87b54af7bd4b643a33197f5c203a622296da910ctree
parent994e6eb72e3475967a9a40a0566744ce1794f20acommit | diff
Fix for iff terms over equalities between the same term and differing constants.
src/theory/booleans/theory_bool_rewriter.cpp diff | blob | history
src/util/cardinality.cpp diff | blob | history
src/util/cardinality.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/constant-rewrite.smt [new file with mode: 0644] blob