Strengthen minisat assertion regarding t-propagations that was unintentionally allowi...

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 1e31e354b43a7516215f81017cfe58e019d27319..ac3c5e1011f33c224d16004c435ef435e7bef725 100644 (file)
--- 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");
     }
   }
 }