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 23d46fd406047379c8f17147430a6d751f42b9d9..24d422909bc70de4c6eb6913142eac14f16f01aa 100644 (file)
--- 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 cc8baa1c0165f65786a33cc31d95e95b26aeb4b9..5e8db2561a8ec2ff31bd90868bc862aaf6f5d62f 100644 (file)
--- 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;