diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-09 14:14:09 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-09 14:14:09 -0500 |
commit | a97944b850f201fd692aa870e830b8fa0369c541 (patch) | |
tree | 7f4ff2086c236b2041ea3546cd82f1af0ba997bc /test/regress | |
parent | a3a436b7b52eee9b6b5c93d58fb84e707b5e832b (diff) |
Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
Diffstat (limited to 'test/regress')
37 files changed, 49 insertions, 36 deletions
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 6078bfa19..7bcd700bd 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -56,7 +56,8 @@ TESTS = \ fmf-nemp-2.smt2 \ trees-1.smt2 \ wand-false.smt2 \ - dup-nemp.smt2 + dup-nemp.smt2 \ + emp2-quant-unsat.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 index d3245e33f..ebe52fa46 100644 --- a/test/regress/regress0/sep/chain-int.smt2 +++ b/test/regress/regress0/sep/chain-int.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 index a0fc5a187..f68434f33 100755 --- a/test/regress/regress0/sep/crash1220.smt2 +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2 index 766354cd9..b3e2088b1 100644 --- a/test/regress/regress0/sep/dispose-list-4-init.smt2 +++ b/test/regress/regress0/sep/dispose-list-4-init.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-sort Loc 0) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 009561128..98348f617 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2 new file mode 100644 index 000000000..52d99d8c0 --- /dev/null +++ b/test/regress/regress0/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)) (not (emp u)))) + +(assert (forall ((x U) (y U)) (= x y))) + +(check-sat) diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2 index 2981606d8..b857aec2a 100644 --- a/test/regress/regress0/sep/loop-1220.smt2 +++ b/test/regress/regress0/sep/loop-1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index e1e21dd10..a0766a7e0 100644 --- a/test/regress/regress0/sep/nemp.smt2 +++ b/test/regress/regress0/sep/nemp.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_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 index 0c93719c9..c807757d1 100755 --- a/test/regress/regress0/sep/nspatial-simp.smt2 +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 index b0dece248..28ed5c47b 100644 --- a/test/regress/regress0/sep/pto-01.smt2 +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 index f0b6d2dee..ab1cea0c8 100644 --- a/test/regress/regress0/sep/pto-02.smt2 +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 index 1734c93bb..9b0afda7a 100644 --- a/test/regress/regress0/sep/pto-04.smt2 +++ b/test/regress/regress0/sep/pto-04.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 index c3330f036..a93fc4db8 100644 --- a/test/regress/regress0/sep/sep-01.smt2 +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 index 403bcf077..6f190d964 100644 --- a/test/regress/regress0/sep/sep-02.smt2 +++ b/test/regress/regress0/sep/sep-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2 index 427c44b50..8dce5acc7 100644 --- a/test/regress/regress0/sep/sep-03.smt2 +++ b/test/regress/regress0/sep/sep-03.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2 index 26a27eb22..356f866c1 100644 --- a/test/regress/regress0/sep/sep-find2.smt2 +++ b/test/regress/regress0/sep/sep-find2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 index 8ddbdd05f..ab12c6461 100644 --- a/test/regress/regress0/sep/sep-neg-1refine.smt2 +++ b/test/regress/regress0/sep/sep-neg-1refine.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2 index 1a69336a8..425e5ce3c 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 index e71e6a51a..7ada6ff06 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2 index 191e7527f..7b6fc69e9 100644 --- a/test/regress/regress0/sep/sep-neg-simple.smt2 +++ b/test/regress/regress0/sep/sep-neg-simple.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2 index f89a9c0ac..53f890b0d 100644 --- a/test/regress/regress0/sep/sep-neg-swap.smt2 +++ b/test/regress/regress0/sep/sep-neg-swap.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2 index 9b4afe36a..3e595b5e9 100644 --- a/test/regress/regress0/sep/sep-nterm-again.smt2 +++ b/test/regress/regress0/sep/sep-nterm-again.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2 index 0178134cb..d4fb0fd52 100644 --- a/test/regress/regress0/sep/sep-nterm-val-model.smt2 +++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 index 772acd981..9522e2420 100644 --- a/test/regress/regress0/sep/sep-plus1.smt2 +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 index 6cdf51294..cedbb53eb 100755 --- a/test/regress/regress0/sep/sep-simp-unc.smt2 +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-sort U 0) (declare-fun x () U) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index fb58b9d10..9239fb770 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 index 0c0b6a9a3..70927ad82 100644 --- a/test/regress/regress0/sep/simple-neg-sat.smt2 +++ b/test/regress/regress0/sep/simple-neg-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 index ed3187a96..10e509e05 100644 --- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 index 1731174fa..1a9e76a8a 100644 --- a/test/regress/regress0/sep/split-find-unsat.smt2 +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 index 0c0ee72ad..fa0aab591 100644 --- a/test/regress/regress0/sep/wand-0526-sat.smt2 +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (declare-fun y () Int) (declare-fun u () Int) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 9b4871323..1d799c8c9 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (assert (wand (emp 0) (emp 0))) (check-sat) diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2 index 642c0a8aa..65500f775 100644 --- a/test/regress/regress0/sep/wand-false.smt2 +++ b/test/regress/regress0/sep/wand-false.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x x) false)) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 index e8ee4252c..0db7330d1 100644 --- a/test/regress/regress0/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_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 index c317e8736..cce0f79e3 100644 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (emp x))) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 index df4bfa6d8..120683f74 100755 --- a/test/regress/regress0/sep/wand-simp-sat.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(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 index 059e91317..c684d16ad 100755 --- a/test/regress/regress0/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 index 95bc85537..c9851661a 100755 --- a/test/regress/regress0/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) (assert (emp x)) |