Fixes for quantifiers + incremental (#2009)

1 files changed, 15 insertions, 5 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5016bd87f..79b7d9a99 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -83,13 +83,23 @@ void TheoryQuantifiers::finishInit()
 }
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
+  if (n.getKind() != FORALL)
+  {
+    return;
+  }
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL ){
-    if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
-      getQuantifiersEngine()->registerQuantifier( n );
-      Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
-    }
+  if (options::cbqi() && !options::recurseCbqi()
+      && TermUtil::hasInstConstAttr(n))
+  {
+    Debug("quantifiers-prereg")
+        << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl;
+    return;
   }
+  // Preregister the quantified formula.
+  // This initializes the modules used for handling n in this user context.
+  getQuantifiersEngine()->preRegisterQuantifier(n);
+  Debug("quantifiers-prereg")
+      << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
 }