More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 18496b173..dd6db951d 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -190,7 +190,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe,
                 success = true;
               }
             }
-          }while( !success && index<32 );
+          }while( !qe->inConflict() && !success && index<32 );
           //mark if we are incomplete
           osuccess = osuccess && success;
         }