projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 63c1d54) | patch
Added a rewrite for iff:
authorClark Barrett <barrett@cs.nyu.edu>
Thu, 14 Mar 2013 00:37:57 +0000 (20:37 -0400)
committerClark Barrett <barrett@cs.nyu.edu>
Thu, 14 Mar 2013 00:37:57 +0000 (20:37 -0400)
commitc03a972a85d565f10953ee58ec809f1751063f8e
treeaf901613c5f58dbfc5e0272167e041d6650497c9tree
parent63c1d547b7598e3dba35f865ba3749c15a105a6fcommit | diff
Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.
src/theory/booleans/theory_bool_rewriter.cpp diff | blob | history