diff options
Diffstat (limited to 'test')
15 files changed, 38 insertions, 23 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d61203ac2..9469e7d61 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -6,9 +6,10 @@ set(regress_0_tests regress0/arith/arith-eq.smt2 regress0/arith/arith-mixed-types-no-tighten.smt2 regress0/arith/arith-mixed-types-tighten.smt2 - regress0/arith/arith-mixed.smt2 + regress0/arith/arith-strict-relaxed.smt2 regress0/arith/arith-strict.smt2 regress0/arith/arith-tighten-1.smt2 + regress0/arith/arith-tighten-2.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 index 661c3f242..38de29734 100644 --- a/test/regress/regress0/arith/arith-eq.smt2 +++ b/test/regress/regress0/arith/arith-eq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_LRA) diff --git a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 index a06621224..2f02c9d1e 100644 --- a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 +++ b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_LIRA) diff --git a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 index 2f737d5c5..627118777 100644 --- a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 +++ b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_LIRA) diff --git a/test/regress/regress0/arith/arith-mixed.smt2 b/test/regress/regress0/arith/arith-strict-relaxed.smt2 index 5869a51bd..fe17aa536 100644 --- a/test/regress/regress0/arith/arith-mixed.smt2 +++ b/test/regress/regress0/arith/arith-strict-relaxed.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_LRA) diff --git a/test/regress/regress0/arith/arith-strict.smt2 b/test/regress/regress0/arith/arith-strict.smt2 index 969cfd0bb..b1477732c 100644 --- a/test/regress/regress0/arith/arith-strict.smt2 +++ b/test/regress/regress0/arith/arith-strict.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_LRA) diff --git a/test/regress/regress0/arith/arith-tighten-1.smt2 b/test/regress/regress0/arith/arith-tighten-1.smt2 index 237d5b144..a8a5234a0 100644 --- a/test/regress/regress0/arith/arith-tighten-1.smt2 +++ b/test/regress/regress0/arith/arith-tighten-1.smt2 @@ -1,17 +1,19 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_LIRA) -(declare-fun n () Int) +(declare-fun i () Int) +(declare-fun j () Int) +(declare-fun x () Real) +(declare-fun y () Real) -; tests tightenings of the form [Int] >= r to [Int] >= ceiling(r) -; where r is a real. -(assert - (and - (>= n 1.5) - (<= n 1.9) - ) -) + + +(assert (= x y)) +(assert (= x (- 2.5 y))) +(assert (>= (+ i j) x)) +(assert (<= j (+ x 0.5))) +(assert (<= i 0)) (check-sat) diff --git a/test/regress/regress0/arith/arith-tighten-2.smt2 b/test/regress/regress0/arith/arith-tighten-2.smt2 new file mode 100644 index 000000000..24eec2977 --- /dev/null +++ b/test/regress/regress0/arith/arith-tighten-2.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_LIA) + +(declare-fun i () Int) +(declare-fun j () Int) + +(assert (> (+ i j) 1)) +(assert (< i 1)) +(assert (< j 1)) + +(check-sat) diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2 index 1a63f265b..e1ca49ac5 100644 --- a/test/regress/regress0/arith/bug569.smt2 +++ b/test/regress/regress0/arith/bug569.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_AUFLIRA) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2 index 1b76e1075..34aa56480 100644 --- a/test/regress/regress0/arith/integers/ackermann4.smt2 +++ b/test/regress/regress0/arith/integers/ackermann4.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_ALIA) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2 index 8b93a3c35..debd29344 100644 --- a/test/regress/regress0/arith/integers/ackermann5.smt2 +++ b/test/regress/regress0/arith/integers/ackermann5.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --ackermann --no-check-models ; EXPECT: sat (set-logic QF_UFLIA) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/arith/integers/ackermann6.smt2 b/test/regress/regress0/arith/integers/ackermann6.smt2 index 62f2f1276..78f5a3658 100644 --- a/test/regress/regress0/arith/integers/ackermann6.smt2 +++ b/test/regress/regress0/arith/integers/ackermann6.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_UFLIA) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2 b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2 index 26796d27b..8101dfdeb 100644 --- a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2 +++ b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: (set-option :incremental false) (set-info :source "The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html. diff --git a/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2 b/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2 index 14000f941..6187be7c1 100644 --- a/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2 +++ b/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: (set-option :incremental false) (set-info :source "SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria Sorea, and Leonardo de Moura. Contact demoura@csl.sri.com for more diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 index 3e10f6aab..4aa162f5b 100644 --- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 +++ b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs +; COMMAND-LINE: (set-option :incremental false) (set-info :source "TTA Startup. Bruno Dutertre (bruno@csl.sri.com)") (set-info :status unsat) |