From d84d67018234bb6bb24dd9183a888892c3bfd4d7 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 14 Feb 2020 00:50:00 -0300 Subject: [PATCH] Forcing rewrite pass rather than asserting if formula has been rewritten (#3748) This ensures that users or developers don't accidentally break the solver either via options or changing the SMT engine flow so that the formula is not rewritten up to a given point. --- src/smt/smt_engine.cpp | 19 +++++-------------- 1 file 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()) -- 2.30.2