diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 16:15:47 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 16:15:47 +0000 |
commit | 7f4e310c1ba02795bae56702e26cf8460f7e212b (patch) | |
tree | c097f8b6d61cb3c5236fc8cc0ed04a20e8de7717 /src/smt | |
parent | 5032c2163edcdfe554bd6d8d2c59bb7e4ecf9325 (diff) |
Fixed compile error
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3d2a971be..652749557 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -868,6 +868,7 @@ void SmtEnginePrivate::nonClausalSimplify() { learnedLiteralNew = constantPropagations.apply(learnedLiteral); if (learnedLiteralNew == learnedLiteral) { break; + } ++d_smt.d_numConstantProps; learnedLiteral = theory::Rewriter::rewrite(learnedLiteralNew); } @@ -968,15 +969,7 @@ void SmtEnginePrivate::nonClausalSimplify() { d_lastSubstitutionPos = pos; ++pos; } - newLeft = constantPropagations.apply((*pos).first); - if (newLeft != (*pos).first) { - newLeft = Rewriter::rewrite(newLeft); - Assert(newLeft == (*pos).second || - (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); - } - Assert(constantPropagations.apply((*pos).second) == (*pos).second); } - #ifdef CVC4_ASSERTIONS // Check data structure invariants: // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations |