From 04d8d1a3336633b0665a29d4a6e25828a6674a36 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 23 Jan 2013 17:00:56 -0500
Subject: partially address bug 486: allow some model inspection of quantifiers

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

(limited to 'src/theory/quantifiers')

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b1a7c9927..b5287fff4 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -93,7 +93,9 @@ 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);
+  }
 }
 
 void TheoryQuantifiers::check(Effort e) {
-- 
cgit v1.2.3