diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-11 18:47:18 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-11 19:08:20 -0400 |
commit | aef9f4e13ddcf2fa48226d98a2a14f9141a761f7 (patch) | |
tree | 1408033093d6baf363bcf4760262d1daf3d7f506 /src/theory/theory_engine.cpp | |
parent | 21c71dd206b2b131ee12c811bd7b0997de07adfa (diff) |
Fix for rewriterules build breakage.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 45c9402ab..33ff18126 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1639,22 +1639,20 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) { void TheoryEngine::checkTheoryAssertionsWithModel() { for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { - if(theoryId != THEORY_REWRITERULES) { - Theory* theory = d_theoryTable[theoryId]; - if(theory && d_logicInfo.isTheoryEnabled(theoryId)) { - for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(), - it_end = theory->facts_end(); - it != it_end; - ++it) { - Node assertion = (*it).assertion; - Node val = getModel()->getValue(assertion); - if(val != d_true) { - stringstream ss; - ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl - << "The fact: " << assertion << endl - << "Model value: " << val << endl; - InternalError(ss.str()); - } + Theory* theory = d_theoryTable[theoryId]; + if(theory && d_logicInfo.isTheoryEnabled(theoryId)) { + for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(), + it_end = theory->facts_end(); + it != it_end; + ++it) { + Node assertion = (*it).assertion; + Node val = getModel()->getValue(assertion); + if(val != d_true) { + stringstream ss; + ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl + << "The fact: " << assertion << endl + << "Model value: " << val << endl; + InternalError(ss.str()); } } } |