diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-11-02 01:48:41 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-11-02 01:48:41 +0000 |
| commit | 161bf31cfa76271542790ec9a2c052e35d6bb1cb (patch) | |
| tree | 4599f90f5307c527a520cc3cf549ec0323fdd5d8 /src/prop/minisat | |
| parent | b335fcb563d61665259248bfc9b74fa807071e6a (diff) | |
fully implement the always-check-again-after-the-output-channel-is-used fix for bug #275. will finally close #275.
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 961ef85c5..8a883b1cb 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -654,6 +654,7 @@ CRef Solver::propagate(TheoryCheckType type) recheck = true; return updateLemmas(); } else { + recheck = proxy->theoryNeedCheck(); return confl; } } |