diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
-rw-r--r-- | test/regress/regress0/nl/tpp-fail-pf-012921.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/circuit-prop.smt2 | 94 | ||||
-rw-r--r-- | test/regress/regress1/bv/min-pp-rewrite-error.smt2 | 4 |
4 files changed, 106 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4cee236c1..b9fb10267 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -709,6 +709,7 @@ set(regress_0_tests regress0/nl/sqrt.smt2 regress0/nl/sqrt2-value.smt2 regress0/nl/subs0-unsat-confirm.smt2 + regress0/nl/tpp-fail-pf-012921.smt2 regress0/nl/very-easy-sat.smt2 regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 @@ -749,6 +750,7 @@ set(regress_0_tests regress0/precedence/xor-and.cvc regress0/precedence/xor-assoc.cvc regress0/precedence/xor-or.cvc + regress0/preprocess/circuit-prop.smt2 regress0/preprocess/preprocess_00.cvc regress0/preprocess/preprocess_01.cvc regress0/preprocess/preprocess_02.cvc @@ -1457,6 +1459,7 @@ set(regress_1_tests regress1/bv/incorrect1.smtv1.smt2 regress1/bv/issue3654.smt2 regress1/bv/issue3776.smt2 + regress1/bv/min-pp-rewrite-error.smt2 regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 diff --git a/test/regress/regress0/nl/tpp-fail-pf-012921.smt2 b/test/regress/regress0/nl/tpp-fail-pf-012921.smt2 new file mode 100644 index 000000000..c97a12074 --- /dev/null +++ b/test/regress/regress0/nl/tpp-fail-pf-012921.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () Real) +(assert (and (> 0.0 x) (not (= 0.0 (/ 0.0 (* 2 x)))))) +(check-sat) diff --git a/test/regress/regress0/preprocess/circuit-prop.smt2 b/test/regress/regress0/preprocess/circuit-prop.smt2 new file mode 100644 index 000000000..69271636d --- /dev/null +++ b/test/regress/regress0/preprocess/circuit-prop.smt2 @@ -0,0 +1,94 @@ +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat + +;;;;; iteEvalThen(true) +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert a) +(assert b) +(assert (not (ite a b c))) +(check-sat) + +(reset) + +;;;;; iteEvalThen(false) +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert a) +(assert (not b)) +(assert (or (ite a b c) d)) +(check-sat) + +(reset) + +;;;;; iteEvalElse(true) +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (not a)) +(assert c) +(assert (not (ite a b c))) +(check-sat) + +(reset) + +;;;;; iteEvalElse(false) +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (not a)) +(assert (not c)) +(assert (or (ite a b c) d)) +(check-sat) + +(reset) + +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert a) +(assert b) +(assert (=> a c)) +(assert (=> b (not c))) +(check-sat) + +(reset) + +(set-logic ALL) +(assert false) +(check-sat) + +(reset) + +(set-logic ALL) +(declare-fun x () Bool) +(declare-fun z () Bool) +(assert (= x z)) +(assert (not x)) +(assert z) +(check-sat) + +(reset) + +(set-logic ALL) +(declare-fun x3 () Bool) +(declare-fun x9 () Bool) +(assert (not x3)) +(assert (or x3 (and x9 x3))) +(check-sat) diff --git a/test/regress/regress1/bv/min-pp-rewrite-error.smt2 b/test/regress/regress1/bv/min-pp-rewrite-error.smt2 new file mode 100644 index 000000000..510612762 --- /dev/null +++ b/test/regress/regress1/bv/min-pp-rewrite-error.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_BV) +(set-info :status unsat) +(declare-fun v2 () (_ BitVec 4)) +(check-sat-assuming ((and (not (= (_ bv1 4) ((_ sign_extend 3) (ite (bvsgt v2 (_ bv0 4)) (_ bv1 1) (_ bv0 1))))) (bvsge (_ bv1 1) (bvnand (_ bv1 1) (ite (= (_ bv1 4) ((_ sign_extend 3) (ite (bvslt v2 (_ bv0 4)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (bvsgt (_ bv0 4) ((_ sign_extend 3) (ite (bvsle (_ bv0 1) (ite (bvsle (_ bv1 1) (ite (bvugt (_ bv1 4) ((_ sign_extend 3) (ite (bvuge v2 (_ bv1 4)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))))))) |