Only put quantifier assertions in model equality engine if fullModel==true

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index a1f8e32fe01c9019bb98d2cd887402c398f51eb2..be6dd5b086b7b50d176708eab34329998d88c4f0 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -92,14 +92,16 @@ Node TheoryQuantifiers::getValue(TNode n) {
   }
 }
 
-void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
-  for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
-    if((*i).assertion.getKind() == kind::NOT) {
-      Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
-      m->assertPredicate((*i).assertion[0], false);
-    } else {
-      Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
-      m->assertPredicate(*i, true);
+void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
+  if(fullModel) {
+    for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
+      if((*i).assertion.getKind() == kind::NOT) {
+        Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
+        m->assertPredicate((*i).assertion[0], false);
+      } else {
+        Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
+        m->assertPredicate(*i, true);
+      }
     }
   }
 }