From: yoni206 <yoni206@users.noreply.github.com>
Date: Fri, 11 Dec 2020 23:08:23 +0000 (-0800)
Subject: bv-to-int: new tests from an issue (#5654)
X-Git-Tag: cvc5-1.0.0~2454
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=107b1422f9549eb2128729c3fd173441029ba443;p=cvc5.git

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 304ea2290..e2851e37a 100644
--- 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
index 000000000..e6ff1cf51
--- /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
index 000000000..1f812a503
--- /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