Abort if in conflict in enumerative instantiation (#4298)

In very rare cases, quantifiers engine can be the first to detect a quantifier-free conflict while constructing term indices. When this occurs, instantiation modules can quit immediately. This was not happening in a case of enumerative instantiation.

Fixes #4293.

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index ce024fe8be6fef5108b04a7ed341a1b5ad0d870d..81ade68fca6c9eddeb513111a20f44b82b8e5817 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -88,6 +88,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
   {
     return;
   }
+  Assert(!d_quantEngine->inConflict());
   double clSet = 0;
   if (Trace.isOn("fs-engine"))
   {
@@ -140,10 +141,10 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
             }
             // added lemma
             addedLemmas++;
-            if (d_quantEngine->inConflict())
-            {
-              break;
-            }
+          }
+          if (d_quantEngine->inConflict())
+          {
+            break;
           }
         }
       }
@@ -324,6 +325,12 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
           {
             index--;
           }
+          if (d_quantEngine->inConflict())
+          {
+            // could be conflicting for an internal reason (such as term
+            // indices computed in above calls)
+            return false;
+          }
         }
       } while (success);
       max_i++;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4339ee75ff798b7e3c160ac2cd3169a295b8ae62..6e60780d6aa3fb241422afe4102bf1710b345a4c 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -601,6 +601,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
           << "  Theory engine finished : " << !theoryEngineNeedsCheck()
           << std::endl;
       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
+      Trace("quant-engine-debug")
+          << "  In conflict : " << d_conflict << std::endl;
     }
     if( Trace.isOn("quant-engine-ee-pre") ){
       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;