summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/minisat/core/Solver.cc2
1 files changed, 1 insertions, 1 deletions
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");
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback