From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 18 Sep 2015 18:13:11 +0000 (+0200)
Subject: Fix bug in quantifiers engine where model construction could be skipped.
X-Git-Tag: cvc5-1.0.0~6236
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b2152c61334b73d26f8e7f6f051f1ae64a2206d;p=cvc5.git

Fix bug in quantifiers engine where model construction could be skipped.
---

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 23d46fd40..24d422909 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -315,6 +315,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
     }
   }
+  Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl;
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
     if( Trace.isOn("quant-engine-debug") ){
@@ -344,7 +345,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     //reset relevant information
-    d_conflict = false;
     d_hasAddedLemma = false;
 
     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
@@ -419,6 +419,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
   }else{
     Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl;
+    d_hasAddedLemma = false;
   }
   //SAT case
   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index cc8baa1c0..5e8db2561 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -172,8 +172,6 @@ private:
   std::map< Node, bool > d_phase_req_waiting;
   /** has added lemma this round */
   bool d_hasAddedLemma;
-  /** has a conflict been found */
-  bool d_conflict;
   /** list of all instantiations produced for each quantifier */
   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
   std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;