new test for resolved issue (#8784)

#8412 is now fixed on main. This PR adds a regression from that issue.
closes #8412 .

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index e11f6d78b5d119d68bdd2b2dd9592e43045e77ec..6c88f29d1192ee16da6fe53ecd541727f22d9b7e 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -277,6 +277,7 @@ set(regress_0_tests
   regress0/bv/bv_to_int_5281.smt2
   regress0/bv/bv_to_int_5293_1.smt2
   regress0/bv/bv_to_int_5293_2.smt2
+  regress0/bv/bv_to_int_8412.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2

diff --git a/test/regress/cli/regress0/bv/bv_to_int_8412.smt2 b/test/regress/cli/regress0/bv/bv_to_int_8412.smt2
new file mode 100644 (file)
index 0000000..3525c5f
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_8412.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-bv-as-int=bitwise
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x () (_ BitVec 2))
+(assert (distinct true (bvule (bvsdiv (_ bv0 2) x) (_ bv0 2))))
+(check-sat)
+