diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-26 21:09:55 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-26 21:09:55 -0500 |
| commit | 5f58ecb6638f0e0fe63b67f1790b997684655bdd (patch) | |
| tree | 32da62448d8f1888c074e2403a7ee9a7ea689399 /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | f837652f6d3a64e31238443b632cc1b7b1b4c804 (diff) | |
another fix for quantifier models (related to bug 486)
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
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); + } } } |