diff options
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 66e05b1cd..a278274c3 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -120,16 +120,24 @@ void TheoryQuantifiers::computeCareGraph() { //do nothing } -void TheoryQuantifiers::collectModelInfo(TheoryModel* m) { +bool TheoryQuantifiers::collectModelInfo(TheoryModel* m) +{ 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); + if (!m->assertPredicate((*i).assertion[0], false)) + { + return false; + } } else { Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; - m->assertPredicate(*i, true); + if (!m->assertPredicate(*i, true)) + { + return false; + } } } + return true; } void TheoryQuantifiers::check(Effort e) { |