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/sat.cpp | |
| 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/sat.cpp')
| -rw-r--r-- | src/prop/sat.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 5d53bf100..36f411df4 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -70,6 +70,10 @@ void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { d_theoryEngine->assertFact(literalNode); } +bool SatSolver::theoryNeedCheck() const { + return d_theoryEngine->needCheck(); +} + void SatSolver::setCnfStream(CnfStream* cnfStream) { d_cnfStream = cnfStream; } |