projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec36649) | patch
Strengthen minisat assertion regarding t-propagations that was unintentionally allowi...
authorMorgan Deters <mdeters@gmail.com>
Fri, 9 Mar 2012 20:30:15 +0000 (20:30 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 9 Mar 2012 20:30:15 +0000 (20:30 +0000)
commitcc5fab5a3e726fefb5cd40335a4ecf210881f0e0
treeeccc607900e5325a44b7fc9dc657a852bb13949ctree
parentec366494778d34d6fd2d27a124a641ebdc249b43commit | diff
Strengthen minisat assertion regarding t-propagations that was unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer).  Credit to Clark for finding this.
src/prop/minisat/core/Solver.cc diff | blob | history