4 files changed, 32 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)
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7d29db744..5d4501309 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2103,6 +2103,8 @@ set(regress_2_tests
   regress2/bug812.smt2
   regress2/bv/opStructure_MBA_6.scrambled.min.smt2
   regress2/bv_to_int2.smt2
+  regress2/bv_to_int_5095.smt2
+  regress2/bv_to_int_5095_2.smt2
   regress2/bv_to_int_ashr.smt2
   regress2/bv_to_int_bitwise.smt2
   regress2/bv_to_int_bvmul1.smt2
diff --git a/test/regress/regress2/bv_to_int_5095.smt2 b/test/regress/regress2/bv_to_int_5095.smt2
new file mode 100644
index 000000000..bec97618d
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_5095.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic QF_BV)
+(set-option :solve-bv-as-int sum)
+(set-option :incremental true)
+(declare-fun _substvar_27_ () Bool)
+(declare-const bv_40-3 (_ BitVec 40))
+(assert (= bv_40-3 (_ bv0 40)))
+(push 1)
+(assert _substvar_27_)
+(check-sat)
+\ No newline at end of file
diff --git a/test/regress/regress2/bv_to_int_5095_2.smt2 b/test/regress/regress2/bv_to_int_5095_2.smt2
new file mode 100644
index 000000000..54dfa0946
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_5095_2.smt2
@@ -0,0 +1,6 @@
+; EXPECT: sat
+; COMMAND --solve-bv-as-int=sum
+(set-logic BV)
+(declare-const bv_42-0 (_ BitVec 42))
+(assert (exists ((q28 (_ BitVec 42))) (distinct (bvudiv bv_42-0 bv_42-0) q28)))
+(check-sat)
+\ No newline at end of file