Make `--solve-int-as-bv=X` robust to rewriting (#6722)

After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.

5 files changed, 43 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 19c689b87..b94e06e47 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -645,6 +645,10 @@ set(regress_0_tests
   regress0/incorrect1.smtv1.smt2
   regress0/ineq_basic.smtv1.smt2
   regress0/ineq_slack.smtv1.smt2
+  regress0/int-to-bv/basic.smt2
+  regress0/int-to-bv/neg-consts.smt2
+  regress0/int-to-bv/not-enough-bits.smt2
+  regress0/int-to-bv/overflow.smt2
   regress0/issue1063-overloading-dt-cons.smt2
   regress0/issue1063-overloading-dt-fun.smt2
   regress0/issue1063-overloading-dt-sel.smt2
diff --git a/test/regress/regress0/int-to-bv/basic.smt2 b/test/regress/regress0/int-to-bv/basic.smt2
new file mode 100644
index 000000000..1e30a7ee8
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/basic.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-int-as-bv=5 --no-check-models
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+; Tests the conversion of negative constants and non-linear multiplication
+(assert (= (- 2) (* x y)))
+; Operators with more than two children
+(assert (= 8 (* x x x)))
+(set-info :status sat)
+(check-sat)
diff --git a/test/regress/regress0/int-to-bv/neg-consts.smt2 b/test/regress/regress0/int-to-bv/neg-consts.smt2
new file mode 100644
index 000000000..46c08dad5
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/neg-consts.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+(assert (> (- 1) x))
+(assert (>= y x))
+(assert (< 0 y))
+(set-info :status sat)
+(check-sat)
diff --git a/test/regress/regress0/int-to-bv/not-enough-bits.smt2 b/test/regress/regress0/int-to-bv/not-enough-bits.smt2
new file mode 100644
index 000000000..49711ecc9
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/not-enough-bits.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-int-as-bv=3
+; SCRUBBER: sed -n "s/.*\(Not enough bits\).*: 4.*/\1/p"
+; EXPECT: Not enough bits
+; EXIT: 1
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+; The negative constant fits, the positive does not
+(assert (= (- 4) (* x y)))
+(assert (= 4 (* x y)))
+(check-sat)
diff --git a/test/regress/regress0/int-to-bv/overflow.smt2 b/test/regress/regress0/int-to-bv/overflow.smt2
new file mode 100644
index 000000000..30e47adb3
--- /dev/null
+++ b/test/regress/regress0/int-to-bv/overflow.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-int-as-bv=4
+; EXPECT: unknown
+(set-logic QF_NIA)
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (- 1) (+ x y)))
+(assert (> x 0))
+(assert (> y 0))
+(check-sat)