diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 6 | ||||
-rw-r--r-- | test/regress/regress0/arith/arith-eq.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 | 18 | ||||
-rw-r--r-- | test/regress/regress0/arith/arith-mixed-types-tighten.smt2 | 32 | ||||
-rw-r--r-- | test/regress/regress0/arith/arith-mixed.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/arith/arith-strict.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress0/arith/arith-tighten-1.smt2 | 17 |
7 files changed, 114 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 20272de2b..35d604768 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -3,6 +3,12 @@ set(regress_0_tests regress0/arith/ackermann.real.smt2 + regress0/arith/arith-eq.smt2 + regress0/arith/arith-mixed.smt2 + regress0/arith/arith-tighten-1.smt2 + regress0/arith/arith-strict.smt2 + regress0/arith/arith-mixed-types-tighten.smt2 + regress0/arith/arith-mixed-types-no-tighten.smt2 regress0/arith/arith.01.cvc regress0/arith/arith.02.cvc regress0/arith/arith.03.cvc diff --git a/test/regress/regress0/arith/arith-eq.smt2 b/test/regress/regress0/arith/arith-eq.smt2 new file mode 100644 index 000000000..661c3f242 --- /dev/null +++ b/test/regress/regress0/arith/arith-eq.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_LRA) + +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun z () Real) + +(assert (= z 0)) +(assert (= (* 3 x) y)) +(assert (= (+ 1 (* 5 x)) y)) +(assert (= (+ 7 (* 4 x)) y)) + +(check-sat) diff --git a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 new file mode 100644 index 000000000..a06621224 --- /dev/null +++ b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_LIRA) + +(declare-fun x () Real) +(declare-fun n () Int) + +; Even though `n` is an integer, this would be UNSAT for real `n`, so the integrality can be ignored. +(assert + (and + (>= (+ x n) 1) + (<= n 0) + (<= x 0) + ) +) + +(check-sat) + diff --git a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 new file mode 100644 index 000000000..2f737d5c5 --- /dev/null +++ b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 @@ -0,0 +1,32 @@ +; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_LIRA) + +(declare-fun x_44 () Real) +(declare-fun x_45 () Real) + +; This test is a subset of one of the `../lemmas` tests. I think `../lemmas/sc_init_frame_gap.induction.smtv1.smt2`. +(declare-fun termITE_30 () Int) +(declare-fun termITE_3 () Real) +(declare-fun termITE_4 () Real) +(declare-fun termITE_8 () Real) +(declare-fun termITE_9 () Real) +(declare-fun termITE_31 () Int) + +(assert + (let ((_let_0 (* (- 1.0) termITE_3))) + (and + (>= (+ termITE_8 (* (- 1.0) termITE_9)) 0.0) + ; This literal can be tightened to `termITE_31 <= 1`. + (not (>= termITE_31 2)) + (>= (+ (* (- 1.0) x_44) (/ termITE_31 1)) 0.0) + (>= (+ x_44 (* (- 1.0) termITE_4)) 0.0) + (not (>= (+ _let_0 (* (/ 1 2) termITE_8)) 0.0)) + (>= (+ (* (- 1.0) x_45) termITE_9) 0.0) + (>= (+ x_45 (/ (* (- 1) termITE_30) 1)) 0.0) + (>= termITE_30 2) + (>= (+ _let_0 termITE_4) 0.0))) +) + +(check-sat) + diff --git a/test/regress/regress0/arith/arith-mixed.smt2 b/test/regress/regress0/arith/arith-mixed.smt2 new file mode 100644 index 000000000..5869a51bd --- /dev/null +++ b/test/regress/regress0/arith/arith-mixed.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_LRA) + +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun z () Real) + +; Both strict and non-strict inequalities. +(assert (< y 0)) +(assert (>= y x)) +(assert (>= y (- x))) + +(check-sat) diff --git a/test/regress/regress0/arith/arith-strict.smt2 b/test/regress/regress0/arith/arith-strict.smt2 new file mode 100644 index 000000000..969cfd0bb --- /dev/null +++ b/test/regress/regress0/arith/arith-strict.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_LRA) + +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun z () Real) + +(assert (< y 0)) +(assert (> y x)) +(assert (> y (- x))) + +(check-sat) diff --git a/test/regress/regress0/arith/arith-tighten-1.smt2 b/test/regress/regress0/arith/arith-tighten-1.smt2 new file mode 100644 index 000000000..237d5b144 --- /dev/null +++ b/test/regress/regress0/arith/arith-tighten-1.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat +(set-logic QF_LIRA) + +(declare-fun n () Int) + +; tests tightenings of the form [Int] >= r to [Int] >= ceiling(r) +; where r is a real. +(assert + (and + (>= n 1.5) + (<= n 1.9) + ) +) + +(check-sat) + |