diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 27 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv-int-collapse1.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv-int-collapse2.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/issue5396.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/issue5736.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress0/issue5743.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/issue5947.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress1/bv/bv2nat-ground.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/bv/issue3958.smt2 | 8 |
9 files changed, 60 insertions, 14 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6036b021b..707e5e43d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -235,6 +235,16 @@ set(regress_0_tests regress0/bv/bug440.smtv1.smt2 regress0/bv/bug733.smt2 regress0/bv/bug734.smt2 + regress0/bv/bv-abstr-bug.smt2 + regress0/bv/bv-abstr-bug2.smt2 + regress0/bv/bv-int-collapse1.smt2 + regress0/bv/bv-int-collapse2.smt2 + regress0/bv/bv-options4.smt2 + regress0/bv/bv-to-bool1.smtv1.smt2 + regress0/bv/bv-to-bool2.smt2 + regress0/bv/bv2nat-ground-c.smt2 + regress0/bv/bv2nat-simp-range.smt2 + regress0/bv/bv_to_int1.smt2 regress0/bv/bv_to_int_5230_binary.smt2 regress0/bv/bv_to_int_5230_missing_op.smt2 regress0/bv/bv_to_int_5230_shift_const.smt2 @@ -242,20 +252,10 @@ set(regress_0_tests 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 + regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 regress0/bv/bv_to_int_elim_err.smt2 regress0/bv/bv_to_int_zext.smt2 - regress0/bv/bv_to_int1.smt2 - regress0/bv/bv-abstr-bug.smt2 - regress0/bv/bv-abstr-bug2.smt2 - regress0/bv/bv-int-collapse1.smt2 - regress0/bv/bv-int-collapse2.smt2 - regress0/bv/bv-options4.smt2 - regress0/bv/bv-to-bool1.smtv1.smt2 - regress0/bv/bv-to-bool2.smt2 - regress0/bv/bv2nat-ground-c.smt2 - regress0/bv/bv2nat-simp-range.smt2 regress0/bv/bvcomp.cvc regress0/bv/bvmul-pow2-only.smt2 regress0/bv/bvsimple.cvc @@ -421,6 +421,7 @@ set(regress_0_tests regress0/bv/issue-4076.smt2 regress0/bv/issue-4130.smt2 regress0/bv/issue3621.smt2 + regress0/bv/issue5396.smt2 regress0/bv/mul-neg-unsat.smt2 regress0/bv/mul-negpow2.smt2 regress0/bv/mult-pow2-negative.smt2 @@ -660,6 +661,9 @@ set(regress_0_tests regress0/issue5540-2-dump-model.smt2 regress0/issue5540-model-decls.smt2 regress0/issue5550-num-children.smt2 + regress0/issue5736.smt2 + regress0/issue5743.smt2 + regress0/issue5947.smt2 regress0/issue6605-2-abd-triv.smt2 regress0/ite_arith.smt2 regress0/ite_real_int_type.smtv1.smt2 @@ -1501,6 +1505,7 @@ set(regress_1_tests regress1/bv/incorrect1.smtv1.smt2 regress1/bv/issue3654.smt2 regress1/bv/issue3776.smt2 + regress1/bv/issue3958.smt2 regress1/bv/min-pp-rewrite-error.smt2 regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2 index a31036f71..1f5015d14 100644 --- a/test/regress/regress0/bv/bv-int-collapse1.smt2 +++ b/test/regress/regress0/bv/bv-int-collapse1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: +; COMMAND-LINE: --bv-solver=lazy ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2 index 5cf6a600c..d56188dad 100644 --- a/test/regress/regress0/bv/bv-int-collapse2.smt2 +++ b/test/regress/regress0/bv/bv-int-collapse2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: +; COMMAND-LINE: --bv-solver=lazy ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/regress0/bv/issue5396.smt2 b/test/regress/regress0/bv/issue5396.smt2 new file mode 100644 index 000000000..7f6d3ab38 --- /dev/null +++ b/test/regress/regress0/bv/issue5396.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_BVLIA) +(set-info :status unsat) +(declare-fun a () Int) +(assert (= (bv2nat (bvor ((_ int2bv 3) a) ((_ int2bv 3) a))) 0)) +(assert (distinct ((_ extract 0 0) (bvsdiv ((_ int2bv 3) (bv2nat (bvmul ((_ int2bv 3) a) ((_ int2bv 3) a)))) ((_ int2bv 3) 1))) (_ bv0 1))) +(check-sat) diff --git a/test/regress/regress0/issue5736.smt2 b/test/regress/regress0/issue5736.smt2 new file mode 100644 index 000000000..dd4d4f951 --- /dev/null +++ b/test/regress/regress0/issue5736.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -q --check-unsat-cores --check-models +(set-info :status sat) +(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32))) +(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32))) +(declare-fun c () (_ BitVec 32)) +(declare-fun d () (_ BitVec 32)) +(declare-fun e () (_ BitVec 32)) +(declare-fun f () (_ BitVec 32)) +(declare-fun g () (Array (_ BitVec 32) (_ BitVec 32))) +(assert (= (= d e) (= (select a c) f))) +(assert (= g (store b (bvxor (_ bv4 32) f) (_ bv0 32)))) +(check-sat) diff --git a/test/regress/regress0/issue5743.smt2 b/test/regress/regress0/issue5743.smt2 new file mode 100644 index 000000000..b53f0fbef --- /dev/null +++ b/test/regress/regress0/issue5743.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --check-models -q +(set-logic QF_AUFBV) +(set-info :status sat) +(declare-fun bv_22-0 () (_ BitVec 1)) +(declare-fun arr-8324605531633220487_-1461211092162269148-0 () (Array (_ BitVec 1) Bool)) +(assert (select arr-8324605531633220487_-1461211092162269148-0 (bvlshr bv_22-0 bv_22-0))) +(check-sat) diff --git a/test/regress/regress0/issue5947.smt2 b/test/regress/regress0/issue5947.smt2 new file mode 100644 index 000000000..4fbcfb00b --- /dev/null +++ b/test/regress/regress0/issue5947.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: -q --check-models +(set-logic QF_UFBVLIA) +(set-info :status sat) +(declare-fun f ((_ BitVec 3)) Int) +(declare-fun x () (_ BitVec 3)) +(declare-fun y () (_ BitVec 3)) +(assert (not (= (f (bvxor x y)) (f (bvxnor x y))))) +(check-sat) diff --git a/test/regress/regress1/bv/bv2nat-ground.smt2 b/test/regress/regress1/bv/bv2nat-ground.smt2 index 50550f530..7e0da282e 100644 --- a/test/regress/regress1/bv/bv2nat-ground.smt2 +++ b/test/regress/regress1/bv/bv2nat-ground.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: +; COMMAND-LINE: --bv-solver=lazy ; EXPECT: unsat (set-logic QF_BVLIA) (set-info :status unsat) diff --git a/test/regress/regress1/bv/issue3958.smt2 b/test/regress/regress1/bv/issue3958.smt2 new file mode 100644 index 000000000..5ed71630d --- /dev/null +++ b/test/regress/regress1/bv/issue3958.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_BV) +(set-info :status sat) +(declare-const v4 Bool) +(declare-const v8 Bool) +(declare-const bv_21-0 (_ BitVec 21)) +(assert (or (= bv_21-0 bv_21-0 bv_21-0 (_ bv0 21) bv_21-0) v4)) +(assert (or (= (_ bv0 21) (bvudiv bv_21-0 bv_21-0) (_ bv0 21) (_ bv0 21)) v8)) +(check-sat) |