diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-12-11 15:08:23 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-11 17:08:23 -0600 |
commit | 107b1422f9549eb2128729c3fd173441029ba443 (patch) | |
tree | 6f34ed2537fac701ba7557b4db7215f3678e9c47 | |
parent | 8d0de294c259e789a149bc5ceb5d6501868e83d0 (diff) |
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 .
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_5293_1.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_5293_2.smt2 | 8 |
3 files changed, 17 insertions, 0 deletions
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 |