From cc5fab5a3e726fefb5cd40335a4ecf210881f0e0 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 9 Mar 2012 20:30:15 +0000 Subject: 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 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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"); } } } -- cgit v1.2.3