diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-15 18:12:40 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-15 18:12:40 +0000 |
commit | a0e91c27c047e7abcfd254584e8a9f27c676b9ed (patch) | |
tree | 5c5d1919a93d57cc9981e87b011550fbf030ceda /src/theory/theory_engine.cpp | |
parent | ceb25a750a29b51645a69bbffc77c86b241ea1f1 (diff) |
d_incomplete is context-dependent; we shouldn't be saving its value and restoring after a flipDecision().
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c32f36275..0f9cb5e8e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -321,15 +321,12 @@ void TheoryEngine::check(Theory::Effort effort) { // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) { if(d_logicInfo.isQuantified()) { - bool prevIncomplete = d_incomplete; // quantifiers engine must pass effort last call check d_quantEngine->check(Theory::EFFORT_LAST_CALL); // if we have given up, then possibly flip decision if(options::flipDecision()) { if(d_incomplete && !d_inConflict && !needCheck()) { - if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) { - d_incomplete = prevIncomplete; - } + ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision(); } } // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built |