diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-01 18:00:12 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 18:06:11 -0500 |
| commit | d6a6ab61dbe64848b78b9ab8d07d95fc58b64e72 (patch) | |
| tree | db3cb085ddd0c2aad7e8ee32cb5d0c4a428183c6 /src/theory/quantifiers | |
| parent | 822d66189bac649d1f04208f8f4f80e292403d40 (diff) | |
Significant work on bug #491 (not yet closed).
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 |
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); } } |