From a0e91c27c047e7abcfd254584e8a9f27c676b9ed Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 15 Nov 2012 18:12:40 +0000 Subject: [PATCH] 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.) --- src/theory/theory_engine.cpp | 5 +---- 1 file changed, 1 insertion(+), 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 -- 2.30.2