From c808605ef15eb79f9ddc2d1a2b4f6dd052530877 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Apr 2020 01:28:18 -0500
Subject: 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.
---
 src/theory/quantifiers/inst_strategy_enumerative.cpp | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'src/theory/quantifiers/inst_strategy_enumerative.cpp')

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index ce024fe8b..81ade68fc 100644
--- 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++;
-- 
cgit v1.2.3