diff options
| -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 |