diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-10-09 13:22:28 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-10-09 13:22:28 +0000 |
| commit | 5b65d0f80d56731fd7d07f491973bad14a85566e (patch) | |
| tree | 4aafa4742804ff87408a1da7523d799851a028c0 /src/prop/minisat | |
| parent | bdaa3049467fd17d3fb95701f7946a4bf0f5206a (diff) | |
* Add assertion in TheoryModel code to ensure we don't get inconsistent
substitutions for solved variables. Related to bug 418 (and might
resolve it).
* Respect phase-locking in Minisat (one phase-saving site was unguarded).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e36589ba8..fbaef61f2 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1443,7 +1443,8 @@ void Solver::pop() Var x = var(trail.last()); assigns [x] = l_Undef; vardata[x].trail_index = -1; - polarity[x] = sign(trail.last()); + if(phase_saving >= 1 && (polarity[x] & 0x2) == 0) + polarity[x] = sign(trail.last()); if(intro_level(x) != -1) {// might be unregistered insertVarOrder(x); } |