diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 19 |
1 files changed, 5 insertions, 14 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4a7c9def3..ad4d4e1d5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3331,24 +3331,15 @@ void SmtEnginePrivate::processAssertions() { d_passes["bv-intro-pow2"]->apply(&d_assertions); } - if (options::unsatCores()) - { - // special rewriting pass for unsat cores, since many of the passes below - // are skipped - d_passes["rewrite"]->apply(&d_assertions); - } - else + // Since this pass is not robust for the information tracking necessary for + // unsat cores, it's only applied if we are not doing unsat core computation + if (!options::unsatCores()) { d_passes["apply-substs"]->apply(&d_assertions); } - // Assertions ARE guaranteed to be rewritten by this point -#ifdef CVC4_ASSERTIONS - for (unsigned i = 0; i < d_assertions.size(); ++i) - { - Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); - } -#endif + // Assertions MUST BE guaranteed to be rewritten by this point + d_passes["rewrite"]->apply(&d_assertions); // Lift bit-vectors of size 1 to bool if (options::bitvectorToBool()) |