diff options
Diffstat (limited to 'test/regress/regress0/sep')
28 files changed, 0 insertions, 431 deletions
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 692390dde..9b6c44fa5 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -21,42 +21,15 @@ MAKEFLAGS = -k TESTS = \ pto-01.smt2 \ pto-02.smt2 \ - pto-04.smt2 \ sep-01.smt2 \ - sep-02.smt2 \ - sep-03.smt2 \ - sep-find2.smt2 \ - sep-neg-nstrict.smt2 \ sep-plus1.smt2 \ - sep-nterm-val-model.smt2 \ - crash1220.smt2 \ nspatial-simp.smt2 \ - sep-neg-1refine.smt2 \ - sep-neg-simple.smt2 \ sep-simp-unsat-emp.smt2 \ - simple-neg-sat.smt2 \ - wand-simp-sat.smt2 \ - wand-simp-sat2.smt2 \ - wand-simp-unsat.smt2 \ - sep-nterm-again.smt2 \ nemp.smt2 \ wand-crash.smt2 \ - wand-nterm-simp.smt2 \ - wand-nterm-simp2.smt2 \ - chain-int.smt2 \ - sep-neg-swap.smt2 \ - sep-neg-nstrict2.smt2 \ - dispose-list-4-init.smt2 \ - wand-0526-sat.smt2 \ - quant_wand.smt2 \ - fmf-nemp-2.smt2 \ trees-1.smt2 \ - wand-false.smt2 \ dup-nemp.smt2 \ - emp2-quant-unsat.smt2 \ dispose-1.smt2 \ - finite-witness-sat.smt2 \ - sep-fmf-priority.smt2 \ nil-no-elim.smt2 diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 deleted file mode 100644 index ebe52fa46..000000000 --- a/test/regress/regress0/sep/chain-int.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(assert (sep (pto x y) (pto y z))) -(assert (and (> x 3) (< x 5))) -(assert (and (> y 3) (< y 5))) -(check-sat) diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 deleted file mode 100644 index f68434f33..000000000 --- a/test/regress/regress0/sep/crash1220.smt2 +++ /dev/null @@ -1,15 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) - -(declare-const x Int) -(declare-const a Int) - -(declare-const y Int) -(declare-const b Int) - -(assert (or (pto x a) (sep (pto x a) (pto y b)))) -(assert (or (not (pto x a)) (sep (not (pto x a)) (not (pto y b))))) - -(check-sat) diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2 deleted file mode 100644 index b3e2088b1..000000000 --- a/test/regress/regress0/sep/dispose-list-4-init.smt2 +++ /dev/null @@ -1,36 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) - -(declare-sort Loc 0) - -(declare-const w Loc) -(declare-const u1 Loc) -(declare-const u2 Loc) -(declare-const u3 Loc) -(declare-const nil Loc) - -(declare-const w1 Loc) -(declare-const w2 Loc) -(declare-const w3 Loc) -(declare-const w4 Loc) - -; allocated (not nil) -(assert (not (= w nil))) -(assert (not (= u1 nil))) -(assert (not (= u2 nil))) -(assert (not (= u3 nil))) -(assert (not (= w1 nil))) -(assert (not (= w2 nil))) -(assert (not (= w4 nil))) - -; from model -;(assert (= w1 u3)) -;(assert (= w2 u2)) -;(assert (= w3 u1)) -;(assert (= w4 u1)) - -(assert (sep (pto w u1) (pto u1 u2) (pto u2 u3) (pto u3 nil))) -(assert (and (sep (sep (pto w4 w1) (pto w1 w2) (pto w2 nil)) (pto w w3)) (sep (pto w w4) true))) - -(check-sat) diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2 deleted file mode 100644 index e89c0fd30..000000000 --- a/test/regress/regress0/sep/emp2-quant-unsat.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -; COMMAND-LINE: --quant-epr -; EXPECT: unsat -(set-logic ALL_SUPPORTED) -(set-info :status unsat) -(declare-sort U 0) -(declare-fun u () U) - -(assert (sep (not (emp u u)) (not (emp u u)))) - -(assert (forall ((x U) (y U)) (= x y))) - -(check-sat) diff --git a/test/regress/regress0/sep/finite-witness-sat.smt2 b/test/regress/regress0/sep/finite-witness-sat.smt2 deleted file mode 100644 index 8aedbfd25..000000000 --- a/test/regress/regress0/sep/finite-witness-sat.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models -; EXPECT: sat -(set-logic ALL_SUPPORTED) -(declare-sort Loc 0) -(declare-const l Loc) - -(assert (not (emp l l))) -(assert (forall ((x Loc) (y Loc)) (not (pto x y)))) - - -(check-sat) diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2 deleted file mode 100644 index 679b1e363..000000000 --- a/test/regress/regress0/sep/fmf-nemp-2.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --finite-model-find --no-check-models -; EXPECT: sat -(set-logic ALL_SUPPORTED) -(declare-sort U 0) -(declare-fun u1 () U) -(declare-fun u2 () U) -(assert (not (= u1 u2))) -(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (emp u1 0)) (pto x 0))))) -; satisfiable with heap of size 2, model of U of size 3 -(check-sat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 deleted file mode 100644 index 9b0afda7a..000000000 --- a/test/regress/regress0/sep/pto-04.smt2 +++ /dev/null @@ -1,36 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const x1 Int) -(declare-const x2 Int) -(declare-const x3 Int) -(declare-const x4 Int) -(declare-const x5 Int) -(declare-const x6 Int) -(declare-const x7 Int) -(declare-const x8 Int) -(declare-const x9 Int) - -(declare-const a1 Int) -(declare-const a2 Int) -(declare-const a3 Int) -(declare-const a4 Int) -(declare-const a5 Int) -(declare-const a6 Int) -(declare-const a7 Int) -(declare-const a8 Int) -(declare-const a9 Int) - -(assert (and (pto x1 a1) (pto x2 a2) (pto x3 a3) - (pto x4 a4) (pto x5 a5) (pto x6 a6) - (pto x7 a7) (pto x8 a8) (pto x9 a9) - ) -) - -(assert (not (and (= x1 x2 x3 x4 x5 x6 x7 x8 x9) - (= a1 a2 a3 a4 a5 a6 a7 a8 a9) - ) - ) -) - -(check-sat) diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2 deleted file mode 100644 index 8a69c10c4..000000000 --- a/test/regress/regress0/sep/quant_wand.smt2 +++ /dev/null @@ -1,15 +0,0 @@ -; COMMAND-LINE: --full-saturate-quant -; EXPECT: unsat -(set-logic ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const u Int) - -(assert (emp 0 0)) - -(assert -(forall ((y Int)) -(not (wand (pto u 5) (and (= y 42) (pto u 5)))) -)) - -(check-sat) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 deleted file mode 100644 index 6f190d964..000000000 --- a/test/regress/regress0/sep/sep-02.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) -(declare-const c Int) - -(assert (sep (pto x a) (pto y b) (pto z c))) - -(assert (or (= x y) (= y z) (= x z))) - -(check-sat) diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2 deleted file mode 100644 index 8dce5acc7..000000000 --- a/test/regress/regress0/sep/sep-03.smt2 +++ /dev/null @@ -1,17 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const x Int) -(declare-const y Int) - -(declare-const a Int) -(declare-const b Int) - -(assert (and (sep (pto x a) (or (pto x a) (pto y b))) - (sep (pto y b) (or (pto x a) (pto y b))) - ) -) - -(assert (not (sep (pto x a) (pto y b)))) - -(check-sat) diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2 deleted file mode 100644 index 356f866c1..000000000 --- a/test/regress/regress0/sep/sep-find2.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const x1 Int) -(declare-const x2 Int) -(declare-const x3 Int) -(declare-const x4 Int) -(declare-const x5 Int) -(declare-const x6 Int) -(declare-const x7 Int) - -(declare-const a1 Int) -(declare-const a2 Int) - -(assert (and -(sep (pto x1 a1) (pto x2 a2) (pto x4 a2) (pto x5 a2) (pto x6 a2) (pto x7 a2)) -(sep (pto x1 a1) (pto x3 a2)) -)) - -(assert (distinct x3 x2 x4 x5 x6 x7)) - -(check-sat) diff --git a/test/regress/regress0/sep/sep-fmf-priority.smt2 b/test/regress/regress0/sep/sep-fmf-priority.smt2 deleted file mode 100644 index fe3af1b35..000000000 --- a/test/regress/regress0/sep/sep-fmf-priority.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models -; EXPECT: sat -(set-logic ALL_SUPPORTED) - -(declare-sort Loc 0) -(declare-const l Loc) -(declare-const x Loc) - -(assert (wand (pto x x) false)) -(assert (forall ((x Loc) (y Loc)) (not (pto x y)))) - -(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 deleted file mode 100644 index ab12c6461..000000000 --- a/test/regress/regress0/sep/sep-neg-1refine.smt2 +++ /dev/null @@ -1,17 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) - -(assert (not (sep (pto x a) (pto y b)))) -(assert (sep (pto x a) (pto z b))) - -; sat with model where y != z -(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2 deleted file mode 100644 index 425e5ce3c..000000000 --- a/test/regress/regress0/sep/sep-neg-nstrict.smt2 +++ /dev/null @@ -1,15 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) - -(assert (not (sep true (pto x a)))) -(assert (sep (pto x a) (pto z b))) - - -(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 deleted file mode 100644 index 7ada6ff06..000000000 --- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) - -(assert (not (= a b))) -(assert (not (sep true (pto x b)))) -(assert (sep (pto x a) (pto z b))) - - -(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2 deleted file mode 100644 index 7b6fc69e9..000000000 --- a/test/regress/regress0/sep/sep-neg-simple.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) - -(assert (not (pto x a))) -(assert (sep (pto x a) (pto z b))) - -(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2 deleted file mode 100644 index 53f890b0d..000000000 --- a/test/regress/regress0/sep/sep-neg-swap.smt2 +++ /dev/null @@ -1,17 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) - -(assert (not (sep (pto y a) (pto x b)))) -(assert (sep (pto x a) (pto y b))) - - -(check-sat) diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2 deleted file mode 100644 index 3e595b5e9..000000000 --- a/test/regress/regress0/sep/sep-nterm-again.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) -(declare-const c Int) - -(assert (and - (not (sep (not (sep (not (pto x a)) (not (pto y b)))) (pto x a) )) - (sep (pto x a) (pto y b)) - ) -) - -(check-sat) diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2 deleted file mode 100644 index d4fb0fd52..000000000 --- a/test/regress/regress0/sep/sep-nterm-val-model.smt2 +++ /dev/null @@ -1,17 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) - -(assert (and - (not (sep (not (pto x a)) (not (pto y b)) )) - (sep (pto x (+ a 1)) (pto y (+ b 1))) - ) -) - -(check-sat) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 deleted file mode 100644 index 70927ad82..000000000 --- a/test/regress/regress0/sep/simple-neg-sat.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) - -(declare-const x Int) -(declare-const y Int) -(declare-const z Int) - -(declare-const a Int) -(declare-const b Int) -(declare-const c Int) - -(assert (and - (not (sep (not (pto x a)) (pto y b) )) - (sep (pto x a) (pto y b)) - ) -) - -(check-sat) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 deleted file mode 100644 index 12aa0a67e..000000000 --- a/test/regress/regress0/sep/wand-0526-sat.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(declare-fun x () Int) -(declare-fun y () Int) -(declare-fun u () Int) -(declare-fun v () Int) -(assert (wand (pto x u) (pto y v))) -(assert (emp 0 0)) -(check-sat) diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2 deleted file mode 100644 index 65500f775..000000000 --- a/test/regress/regress0/sep/wand-false.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) -(declare-fun x () Int) -(assert (wand (pto x x) false)) -(check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 deleted file mode 100644 index b59b53b58..000000000 --- a/test/regress/regress0/sep/wand-nterm-simp.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(declare-fun x () Int) -(assert (wand (emp x x) (pto x 3))) -(check-sat) - diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2 deleted file mode 100644 index fa6a83143..000000000 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) -(declare-fun x () Int) -(assert (wand (pto x 1) (emp x x))) -(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 deleted file mode 100644 index 120683f74..000000000 --- a/test/regress/regress0/sep/wand-simp-sat.smt2 +++ /dev/null @@ -1,6 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(declare-fun x () Int) -(assert (wand (pto x 1) (pto x 1))) -(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2 deleted file mode 100644 index c684d16ad..000000000 --- a/test/regress/regress0/sep/wand-simp-sat2.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) -(declare-fun x () Int) -(assert (wand (pto x 1) (pto x 3))) -(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 deleted file mode 100644 index 850be7b97..000000000 --- a/test/regress/regress0/sep/wand-simp-unsat.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: unsat -(set-logic QF_ALL_SUPPORTED) -(declare-fun x () Int) -(assert (wand (pto x 1) (pto x 3))) -(assert (emp x x)) -(check-sat) |