diff options
Diffstat (limited to 'test/regress/regress1/sep')
28 files changed, 432 insertions, 1 deletions
diff --git a/test/regress/regress1/sep/Makefile.am b/test/regress/regress1/sep/Makefile.am index 3bf63ff1a..bda7e4484 100644 --- a/test/regress/regress1/sep/Makefile.am +++ b/test/regress/regress1/sep/Makefile.am @@ -20,7 +20,34 @@ TESTS = \ loop-1220.smt2 \ sep-simp-unc.smt2 \ split-find-unsat.smt2 \ - split-find-unsat-w-emp.smt2 + split-find-unsat-w-emp.smt2 \ + dispose-list-4-init.smt2 \ + finite-witness-sat.smt2 \ + sep-find2.smt2 \ + sep-fmf-priority.smt2 \ + sep-neg-1refine.smt2 \ + sep-nterm-again.smt2 \ + chain-int.smt2 \ + crash1220.smt2 \ + emp2-quant-unsat.smt2 \ + fmf-nemp-2.smt2 \ + pto-04.smt2 \ + quant_wand.smt2 \ + sep-02.smt2 \ + sep-03.smt2 \ + sep-neg-nstrict.smt2 \ + sep-neg-nstrict2.smt2 \ + sep-neg-simple.smt2 \ + sep-neg-swap.smt2 \ + sep-nterm-val-model.smt2 \ + simple-neg-sat.smt2 \ + wand-0526-sat.smt2 \ + wand-false.smt2 \ + wand-nterm-simp.smt2 \ + wand-nterm-simp2.smt2 \ + wand-simp-sat.smt2 \ + wand-simp-sat2.smt2 \ + wand-simp-unsat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/sep/chain-int.smt2 b/test/regress/regress1/sep/chain-int.smt2 new file mode 100644 index 000000000..ebe52fa46 --- /dev/null +++ b/test/regress/regress1/sep/chain-int.smt2 @@ -0,0 +1,11 @@ +(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/regress1/sep/crash1220.smt2 b/test/regress/regress1/sep/crash1220.smt2 new file mode 100644 index 000000000..f68434f33 --- /dev/null +++ b/test/regress/regress1/sep/crash1220.smt2 @@ -0,0 +1,15 @@ +; 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/regress1/sep/dispose-list-4-init.smt2 b/test/regress/regress1/sep/dispose-list-4-init.smt2 new file mode 100644 index 000000000..b3e2088b1 --- /dev/null +++ b/test/regress/regress1/sep/dispose-list-4-init.smt2 @@ -0,0 +1,36 @@ +; 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/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2 new file mode 100644 index 000000000..e89c0fd30 --- /dev/null +++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2 @@ -0,0 +1,12 @@ +; 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/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2 new file mode 100644 index 000000000..8aedbfd25 --- /dev/null +++ b/test/regress/regress1/sep/finite-witness-sat.smt2 @@ -0,0 +1,11 @@ +; 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/regress1/sep/fmf-nemp-2.smt2 b/test/regress/regress1/sep/fmf-nemp-2.smt2 new file mode 100644 index 000000000..679b1e363 --- /dev/null +++ b/test/regress/regress1/sep/fmf-nemp-2.smt2 @@ -0,0 +1,10 @@ +; 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/regress1/sep/pto-04.smt2 b/test/regress/regress1/sep/pto-04.smt2 new file mode 100644 index 000000000..9b0afda7a --- /dev/null +++ b/test/regress/regress1/sep/pto-04.smt2 @@ -0,0 +1,36 @@ +(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/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2 new file mode 100644 index 000000000..8a69c10c4 --- /dev/null +++ b/test/regress/regress1/sep/quant_wand.smt2 @@ -0,0 +1,15 @@ +; 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/regress1/sep/sep-02.smt2 b/test/regress/regress1/sep/sep-02.smt2 new file mode 100644 index 000000000..6f190d964 --- /dev/null +++ b/test/regress/regress1/sep/sep-02.smt2 @@ -0,0 +1,16 @@ +(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/regress1/sep/sep-03.smt2 b/test/regress/regress1/sep/sep-03.smt2 new file mode 100644 index 000000000..8dce5acc7 --- /dev/null +++ b/test/regress/regress1/sep/sep-03.smt2 @@ -0,0 +1,17 @@ +(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/regress1/sep/sep-find2.smt2 b/test/regress/regress1/sep/sep-find2.smt2 new file mode 100644 index 000000000..356f866c1 --- /dev/null +++ b/test/regress/regress1/sep/sep-find2.smt2 @@ -0,0 +1,22 @@ +(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/regress1/sep/sep-fmf-priority.smt2 b/test/regress/regress1/sep/sep-fmf-priority.smt2 new file mode 100644 index 000000000..fe3af1b35 --- /dev/null +++ b/test/regress/regress1/sep/sep-fmf-priority.smt2 @@ -0,0 +1,12 @@ +; 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/regress1/sep/sep-neg-1refine.smt2 b/test/regress/regress1/sep/sep-neg-1refine.smt2 new file mode 100644 index 000000000..ab12c6461 --- /dev/null +++ b/test/regress/regress1/sep/sep-neg-1refine.smt2 @@ -0,0 +1,17 @@ +; 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/regress1/sep/sep-neg-nstrict.smt2 b/test/regress/regress1/sep/sep-neg-nstrict.smt2 new file mode 100644 index 000000000..425e5ce3c --- /dev/null +++ b/test/regress/regress1/sep/sep-neg-nstrict.smt2 @@ -0,0 +1,15 @@ +(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/regress1/sep/sep-neg-nstrict2.smt2 b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 new file mode 100644 index 000000000..7ada6ff06 --- /dev/null +++ b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 @@ -0,0 +1,18 @@ +; 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/regress1/sep/sep-neg-simple.smt2 b/test/regress/regress1/sep/sep-neg-simple.smt2 new file mode 100644 index 000000000..7b6fc69e9 --- /dev/null +++ b/test/regress/regress1/sep/sep-neg-simple.smt2 @@ -0,0 +1,16 @@ +; 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/regress1/sep/sep-neg-swap.smt2 b/test/regress/regress1/sep/sep-neg-swap.smt2 new file mode 100644 index 000000000..53f890b0d --- /dev/null +++ b/test/regress/regress1/sep/sep-neg-swap.smt2 @@ -0,0 +1,17 @@ +; 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/regress1/sep/sep-nterm-again.smt2 b/test/regress/regress1/sep/sep-nterm-again.smt2 new file mode 100644 index 000000000..3e595b5e9 --- /dev/null +++ b/test/regress/regress1/sep/sep-nterm-again.smt2 @@ -0,0 +1,20 @@ +; 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/regress1/sep/sep-nterm-val-model.smt2 b/test/regress/regress1/sep/sep-nterm-val-model.smt2 new file mode 100644 index 000000000..d4fb0fd52 --- /dev/null +++ b/test/regress/regress1/sep/sep-nterm-val-model.smt2 @@ -0,0 +1,17 @@ +(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/regress1/sep/simple-neg-sat.smt2 b/test/regress/regress1/sep/simple-neg-sat.smt2 new file mode 100644 index 000000000..70927ad82 --- /dev/null +++ b/test/regress/regress1/sep/simple-neg-sat.smt2 @@ -0,0 +1,20 @@ +; 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/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2 new file mode 100644 index 000000000..12aa0a67e --- /dev/null +++ b/test/regress/regress1/sep/wand-0526-sat.smt2 @@ -0,0 +1,10 @@ +; 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/regress1/sep/wand-false.smt2 b/test/regress/regress1/sep/wand-false.smt2 new file mode 100644 index 000000000..65500f775 --- /dev/null +++ b/test/regress/regress1/sep/wand-false.smt2 @@ -0,0 +1,7 @@ +; 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/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2 new file mode 100644 index 000000000..b59b53b58 --- /dev/null +++ b/test/regress/regress1/sep/wand-nterm-simp.smt2 @@ -0,0 +1,7 @@ +; 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/regress1/sep/wand-nterm-simp2.smt2 b/test/regress/regress1/sep/wand-nterm-simp2.smt2 new file mode 100644 index 000000000..fa6a83143 --- /dev/null +++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2 @@ -0,0 +1,7 @@ +; 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/regress1/sep/wand-simp-sat.smt2 b/test/regress/regress1/sep/wand-simp-sat.smt2 new file mode 100644 index 000000000..120683f74 --- /dev/null +++ b/test/regress/regress1/sep/wand-simp-sat.smt2 @@ -0,0 +1,6 @@ +; 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/regress1/sep/wand-simp-sat2.smt2 b/test/regress/regress1/sep/wand-simp-sat2.smt2 new file mode 100644 index 000000000..c684d16ad --- /dev/null +++ b/test/regress/regress1/sep/wand-simp-sat2.smt2 @@ -0,0 +1,7 @@ +; 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/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2 new file mode 100644 index 000000000..850be7b97 --- /dev/null +++ b/test/regress/regress1/sep/wand-simp-unsat.smt2 @@ -0,0 +1,7 @@ +; 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) |