bv-to-int: new tests from an issue (#5654)

#5293 pointed to assertion failures when employing --bv-to-int, starting from commit 94e3d9a.
The bug is not reproduced on current master, and so we would have this PR close #5293 .
This PR adds the benchmarks from #5293 .

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 304ea2290bfa112c7db72c4c10928d750405400a..e2851e37a7c1b0796f894b2eb490e193e2de4f6e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -235,6 +235,8 @@ set(regress_0_tests
   regress0/bv/bv_to_int_5230_missing_op.smt2
   regress0/bv/bv_to_int_5230_shift_const.smt2
   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_bvmul2.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2

diff --git a/test/regress/regress0/bv/bv_to_int_5293_1.smt2 b/test/regress/regress0/bv/bv_to_int_5293_1.smt2
new file mode 100644 (file)
index 0000000..e6ff1cf
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_5293_1.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic UFBV)
+(set-option :solve-bv-as-int sum)
+(declare-const bv_56-0 (_ BitVec 56))
+(assert (forall ((q2 (_ BitVec 7)) (q3 (_ BitVec 56)) (q4 (_ BitVec 56))) (=> (bvugt q4 (bvudiv bv_56-0 bv_56-0)) false)))
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/bv/bv_to_int_5293_2.smt2 b/test/regress/regress0/bv/bv_to_int_5293_2.smt2
new file mode 100644 (file)
index 0000000..1f812a5
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_5293_2.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-option :solve-bv-as-int sum)
+(declare-const v4 Bool)
+(declare-const bv_34-0 (_ BitVec 34))
+(assert (or (not (forall ((q26 Bool) (q27 (_ BitVec 4)) (q28 Bool) (q29 (_ BitVec 4)) (q30 (_ BitVec 34)) (q31 (_ BitVec 38))) (xor (= #x9 #x9 q29 (_ bv11 4) #x9) (= q30 (bvudiv bv_34-0 bv_34-0) bv_34-0 (bvudiv bv_34-0 bv_34-0) (bvudiv bv_34-0 bv_34-0)) (not v4)))) (not (forall ((q26 Bool) (q27 (_ BitVec 4)) (q28 Bool) (q29 (_ BitVec 4)) (q30 (_ BitVec 34)) (q31 (_ BitVec 38))) (xor (= #x9 #x9 q29 (_ bv11 4) #x9) (= q30 (bvudiv bv_34-0 bv_34-0) bv_34-0 (bvudiv bv_34-0 bv_34-0) (bvudiv bv_34-0 bv_34-0)) (not v4))))))
+(check-sat)
\ No newline at end of file