diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/process_assertions.cpp | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 971288b67..719165048 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -201,16 +201,6 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["bv-intro-pow2"]->apply(&assertions); } - // 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(&assertions); - } - - // Assertions MUST BE guaranteed to be rewritten by this point - d_passes["rewrite"]->apply(&assertions); - // Lift bit-vectors of size 1 to bool if (options::bitvectorToBool()) { @@ -219,8 +209,22 @@ bool ProcessAssertions::apply(Assertions& as) if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { d_passes["bv-to-int"]->apply(&assertions); + // after running bv-to-int, we need to immediately run + // theory-preprocess and ite-removal so that newlly created + // terms and assertions are normalized (e.g., div is expanded). + d_passes["theory-preprocess"]->apply(&assertions); } + // 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(&assertions); + } + + // Assertions MUST BE guaranteed to be rewritten by this point + d_passes["rewrite"]->apply(&assertions); + // Convert non-top-level Booleans to bit-vectors of size 1 if (options::boolToBitvector() != options::BoolToBVMode::OFF) { |