From 5aa526ab1df69783d17750bfce8819a6e358e157 Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 6 Oct 2020 13:47:58 -0700
Subject: [PATCH] bv-to-int: change order of passes (#5208)

Closes #5095 and replaces #5110.
There are two tests in #5095 that produce two different assertion failures when using bv-to-int.
The first happens because the substitution map wasn't applied after the pass.
The second happens because div (that is introduced in the pass) is not rewritten using witness.
Both problems are solved by making sure that apply-substs, theory-preprocess and ite-removal are executed after bv-to-int.
The two tests from #5095 are included as regressions.
---
 src/smt/process_assertions.cpp              | 24 ++++++++++++---------
 test/regress/CMakeLists.txt                 |  2 ++
 test/regress/regress2/bv_to_int_5095.smt2   | 10 +++++++++
 test/regress/regress2/bv_to_int_5095_2.smt2 |  6 ++++++
 4 files changed, 32 insertions(+), 10 deletions(-)
 create mode 100644 test/regress/regress2/bv_to_int_5095.smt2
 create mode 100644 test/regress/regress2/bv_to_int_5095_2.smt2

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
-- 
2.30.2