summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 2e33c7c4a..a1f8e32fe 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -95,8 +95,10 @@ 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) {
+ Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
m->assertPredicate((*i).assertion[0], false);
} else {
+ Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
m->assertPredicate(*i, true);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback