diff options
author | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
---|---|---|
committer | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
commit | 36a0d1d948f201471596e092136c5a00103f78af (patch) | |
tree | 7a9b0d79074da1cb0c1cbed986584d50792a30e9 /test/regress/regress0/sep | |
parent | 66525e81928d0d025dbcc197ab3ef772eac31103 (diff) | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4.git
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
Diffstat (limited to 'test/regress/regress0/sep')
36 files changed, 608 insertions, 0 deletions
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) |