diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-09 20:30:15 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-09 20:30:15 +0000 |
commit | cc5fab5a3e726fefb5cd40335a4ecf210881f0e0 (patch) | |
tree | eccc607900e5325a44b7fc9dc657a852bb13949c | |
parent | ec366494778d34d6fd2d27a124a641ebdc249b43 (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.
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 |
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"); } } } |