diff options
Diffstat (limited to 'test')
38 files changed, 610 insertions, 1 deletions
diff --git a/test/Makefile.am b/test/Makefile.am index dcb58b591..931228f41 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -59,6 +59,7 @@ subdirs_to_check = \ regress/regress0/sets \ regress/regress0/parser \ regress/regress0/sygus \ + regress/regress0/sep \ regress/regress1 \ regress/regress1/arith \ regress/regress2 \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 7d7690d22..45842065f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus sep DIST_SUBDIRS = $(SUBDIRS) # don't override a BINARY imported from a personal.mk diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am new file mode 100644 index 000000000..9d2abaa18 --- /dev/null +++ b/test/regress/regress0/sep/Makefile.am @@ -0,0 +1,76 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +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-unc.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 \ + split-find-unsat.smt2 \ + split-find-unsat-w-emp.smt2 \ + nemp.smt2 \ + wand-crash.smt2 \ + wand-nterm-simp.smt2 \ + wand-nterm-simp2.smt2 \ + loop-1220.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 + + +FAILING_TESTS = +# loop-1220.smt2 (slow) + +EXTRA_DIST = $(TESTS) + +# slow after changes on Nov 20 : artemis-0512-nonterm.smt2 +# slow after decision engine respects requirePhase: type003.smt2 loop007.smt2 + +# and make sure to distribute it +EXTRA_DIST += + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 new file mode 100644 index 000000000..d3245e33f --- /dev/null +++ b/test/regress/regress0/sep/chain-int.smt2 @@ -0,0 +1,11 @@ +(set-logic 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 new file mode 100755 index 000000000..a0fc5a187 --- /dev/null +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100644 index 000000000..766354cd9 --- /dev/null +++ b/test/regress/regress0/sep/dispose-list-4-init.smt2 @@ -0,0 +1,36 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2 new file mode 100644 index 000000000..71fe96d71 --- /dev/null +++ b/test/regress/regress0/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)) (pto x 0))))) +; satisfiable with heap of size 2, model of U of size 3 +(check-sat) diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2 new file mode 100644 index 000000000..2981606d8 --- /dev/null +++ b/test/regress/regress0/sep/loop-1220.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const a Int) + +(declare-const y Int) +(declare-const b Int) +(declare-const y0 Int) +(declare-const b0 Int) +(declare-const y00 Int) +(declare-const b00 Int) + +(assert (or false (sep (pto x a) (or false (sep (pto y b) (or false (sep (pto y0 b0) (pto y00 b00) ))))))) +(assert (not (or false (sep (pto x a) (not (or false (sep (pto y b) (not (or false (sep (pto y0 b0) (not (pto y00 b00)) )))))))))) + +(check-sat) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 new file mode 100644 index 000000000..e1e21dd10 --- /dev/null +++ b/test/regress/regress0/sep/nemp.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(assert (not (emp 0))) +(check-sat) diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2 new file mode 100755 index 000000000..0c93719c9 --- /dev/null +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun x () Int) + +(assert (sep (= x 0) (not (= x 5)))) + +(declare-fun y () Int) +(assert (pto y 0)) +(check-sat) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 new file mode 100644 index 000000000..b0dece248 --- /dev/null +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (and (pto x a) (pto x b))) + +(assert (not (= a b))) + +(check-sat) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 new file mode 100644 index 000000000..f0b6d2dee --- /dev/null +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -0,0 +1,25 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + + +(declare-const x 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 x a1) (pto x a2) (pto x a3) + (pto x a4) (pto x a5) (pto x a6) + (pto x a7) (pto x a8) (pto x a9) + ) +) + +(assert (not (= a1 a2 a3 a4 a5 a6 a7 a8 a9))) + +(check-sat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 new file mode 100644 index 000000000..1734c93bb --- /dev/null +++ b/test/regress/regress0/sep/pto-04.smt2 @@ -0,0 +1,36 @@ +(set-logic 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 new file mode 100644 index 000000000..d71b937fc --- /dev/null +++ b/test/regress/regress0/sep/quant_wand.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --cbqi-all +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const u Int) + +(assert (emp 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-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 new file mode 100644 index 000000000..c3330f036 --- /dev/null +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (sep (pto x a) (pto y b))) + +(assert (= x y)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 new file mode 100644 index 000000000..403bcf077 --- /dev/null +++ b/test/regress/regress0/sep/sep-02.smt2 @@ -0,0 +1,16 @@ +(set-logic 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 new file mode 100644 index 000000000..427c44b50 --- /dev/null +++ b/test/regress/regress0/sep/sep-03.smt2 @@ -0,0 +1,17 @@ +(set-logic 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 new file mode 100644 index 000000000..26a27eb22 --- /dev/null +++ b/test/regress/regress0/sep/sep-find2.smt2 @@ -0,0 +1,22 @@ +(set-logic 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-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 new file mode 100644 index 000000000..8ddbdd05f --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-1refine.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100644 index 000000000..1a69336a8 --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2 @@ -0,0 +1,15 @@ +(set-logic 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 new file mode 100644 index 000000000..e71e6a51a --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100644 index 000000000..191e7527f --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-simple.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100644 index 000000000..f89a9c0ac --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-swap.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100644 index 000000000..9b4afe36a --- /dev/null +++ b/test/regress/regress0/sep/sep-nterm-again.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100644 index 000000000..0178134cb --- /dev/null +++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2 @@ -0,0 +1,17 @@ +(set-logic 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/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 new file mode 100644 index 000000000..772acd981 --- /dev/null +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -0,0 +1,18 @@ +(set-logic 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 (and + (sep (pto x a) true) + (sep (pto y (+ a 1)) true) +)) +(assert (= x y)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 new file mode 100755 index 000000000..6cdf51294 --- /dev/null +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun a () U) +(declare-fun b () U) + +(assert (not (sep (not (pto x a)) (pto y b)))) +(check-sat) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 new file mode 100644 index 000000000..fb58b9d10 --- /dev/null +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun a () U) +(declare-fun b () U) + +(assert (emp x)) +(assert (sep (pto x a) (pto y b))) +(check-sat) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 new file mode 100644 index 000000000..0c0b6a9a3 --- /dev/null +++ b/test/regress/regress0/sep/simple-neg-sat.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 new file mode 100644 index 000000000..ed3187a96 --- /dev/null +++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 @@ -0,0 +1,18 @@ +(set-logic 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 (and + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (emp x)) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 new file mode 100644 index 000000000..54530cbf4 --- /dev/null +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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)) (not (pto y b)) (not (sep (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 new file mode 100644 index 000000000..0c0ee72ad --- /dev/null +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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)) +(check-sat) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 new file mode 100644 index 000000000..9b4871323 --- /dev/null +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(assert (wand (emp 0) (emp 0))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 new file mode 100644 index 000000000..e8ee4252c --- /dev/null +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (emp 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 new file mode 100644 index 000000000..69305e95c --- /dev/null +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (emp x))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 new file mode 100755 index 000000000..df4bfa6d8 --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-sat.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic 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 new file mode 100755 index 000000000..ebc115fdd --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(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 new file mode 100755 index 000000000..95bc85537 --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (pto x 3))) +(assert (emp x)) +(check-sat) |