From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 9 Mar 2012 20:30:15 +0000 (+0000)
Subject: Strengthen minisat assertion regarding t-propagations that was unintentionally allowi... 
X-Git-Tag: cvc5-1.0.0~8277
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cc5fab5a3e726fefb5cd40335a4ecf210881f0e0;p=cvc5.git

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.
---

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 1e31e354b..ac3c5e101 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -722,7 +722,7 @@ void Solver::propagateTheory() {
       // but we check that this is the case and that they agree
       Debug("minisat") << "trail_index(var(p)) == " << trail_index(var(p)) << std::endl;
       Assert(trail_index(var(p)) >= oldTrailSize);
-      Assert(value(p) == lbool(!sign(p)));
+      Assert(value(p) == l_True, "a literal was theory-propagated, and so was its negation");
     }
   }
 }