From 5f58ecb6638f0e0fe63b67f1790b997684655bdd Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 26 Jan 2013 21:09:55 -0500
Subject: [PATCH] another fix for quantifier models (related to bug 486)

---
 src/theory/quantifiers/theory_quantifiers.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b5287fff4..2e33c7c4a 100644
--- 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);
+    }
   }
 }
 
-- 
2.30.2