fix for finite model finding caused by new collectModelInfo code

2 files changed, 8 insertions, 6 deletions

diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index d250bee74..1daa30981 100644
--- 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 2e33c7c4a..d1dbae90c 100644
--- 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);
+      }
     }
   }
 }