fix for finite model finding caused by new collectModelInfo code

diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index d250bee74a3bb8f833bc796ccc115feccc6f3261..1daa30981d6c5398d603249a73820c3734493470 100644 (file)
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -11,7 +11,7 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory
 # cdr( nil ) has no set value.
 expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true
  disable rewriting incorrectly applied selectors to arbitrary ground term
-expert-option dtForceAssignment /--dt-force-assignment bool :default false :read-write
+option dtForceAssignment /--dt-force-assignment bool :default false :read-write
  force the datatypes solver to give specific values to all datatypes terms before answering sat
  
 endmodule

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 2e33c7c4a7c136fddc61cb9b8e233cebfe8eb0cf..d1dbae90c21af1686b4940ae0eb48fba2a1b9dc0 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -93,11 +93,13 @@ 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) {
-      m->assertPredicate((*i).assertion[0], false);
-    } else {
-      m->assertPredicate(*i, true);
+  if( fullModel ){
+    for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
+      if((*i).assertion.getKind() == kind::NOT) {
+        m->assertPredicate((*i).assertion[0], false);
+      } else {
+        m->assertPredicate(*i, true);
+      }
     }
   }
 }