another fix for quantifier models (related to bug 486)

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b5287fff4a2503363f7d338f69494113b361d912..2e33c7c4a7c136fddc61cb9b8e233cebfe8eb0cf 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -94,7 +94,11 @@ Node TheoryQuantifiers::getValue(TNode n) {
 
 void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
-    m->assertPredicate(*i, true);
+    if((*i).assertion.getKind() == kind::NOT) {
+      m->assertPredicate((*i).assertion[0], false);
+    } else {
+      m->assertPredicate(*i, true);
+    }
   }
 }