From 107b1422f9549eb2128729c3fd173441029ba443 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 11 Dec 2020 15:08:23 -0800 Subject: [PATCH] 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 . --- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/bv/bv_to_int_5293_1.smt2 | 7 +++++++ test/regress/regress0/bv/bv_to_int_5293_2.smt2 | 8 ++++++++ 3 files changed, 17 insertions(+) create mode 100644 test/regress/regress0/bv/bv_to_int_5293_1.smt2 create mode 100644 test/regress/regress0/bv/bv_to_int_5293_2.smt2 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 -- 2.30.2