From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 15 Nov 2012 18:12:40 +0000 (+0000)
Subject: d_incomplete is context-dependent; we shouldn't be saving its value and restoring... 
X-Git-Tag: cvc5-1.0.0~7591
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0e91c27c047e7abcfd254584e8a9f27c676b9ed;p=cvc5.git

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.)
---

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