From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 27 Jan 2013 02:09:55 +0000 (-0500)
Subject: another fix for quantifier models (related to bug 486)
X-Git-Tag: cvc5-1.0.0~7391^2~26
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f58ecb6638f0e0fe63b67f1790b997684655bdd;p=cvc5.git

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 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);
+    }
   }
 }