diff options
Diffstat (limited to 'test/regress/regress1/sep')
30 files changed, 30 insertions, 30 deletions
diff --git a/test/regress/regress1/sep/chain-int.smt2 b/test/regress/regress1/sep/chain-int.smt2 index 6aaca31c5..14cd98ae2 100644 --- a/test/regress/regress1/sep/chain-int.smt2 +++ b/test/regress/regress1/sep/chain-int.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/crash1220.smt2 b/test/regress/regress1/sep/crash1220.smt2 index 4df23fd80..241f69b77 100644 --- a/test/regress/regress1/sep/crash1220.smt2 +++ b/test/regress/regress1/sep/crash1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/dispose-list-4-init.smt2 b/test/regress/regress1/sep/dispose-list-4-init.smt2 index 0ee63cc8a..e9915bf4b 100644 --- a/test/regress/regress1/sep/dispose-list-4-init.smt2 +++ b/test/regress/regress1/sep/dispose-list-4-init.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-sort Loc 0) (declare-heap (Loc Loc)) diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2 index a0921aa31..cdca1a909 100644 --- a/test/regress/regress1/sep/emp2-quant-unsat.smt2 +++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --quant-epr ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun u () U) diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2 index ce16e6f14..479dbe2b2 100644 --- a/test/regress/regress1/sep/finite-witness-sat.smt2 +++ b/test/regress/regress1/sep/finite-witness-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --quant-epr ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort Loc 0) (declare-const l Loc) (declare-heap (Loc Loc)) diff --git a/test/regress/regress1/sep/fmf-nemp-2.smt2 b/test/regress/regress1/sep/fmf-nemp-2.smt2 index 49420145e..e6e2aca98 100644 --- a/test/regress/regress1/sep/fmf-nemp-2.smt2 +++ b/test/regress/regress1/sep/fmf-nemp-2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort U 0) (declare-heap (U Int)) (declare-fun u1 () U) diff --git a/test/regress/regress1/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2 index 41078391a..c6d239ec0 100644 --- a/test/regress/regress1/sep/loop-1220.smt2 +++ b/test/regress/regress1/sep/loop-1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/pto-04.smt2 b/test/regress/regress1/sep/pto-04.smt2 index e3d3ea7a1..7c430da06 100644 --- a/test/regress/regress1/sep/pto-04.smt2 +++ b/test/regress/regress1/sep/pto-04.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2 index bb4e40308..87f0a974b 100644 --- a/test/regress/regress1/sep/quant_wand.smt2 +++ b/test/regress/regress1/sep/quant_wand.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-02.smt2 b/test/regress/regress1/sep/sep-02.smt2 index a67394d90..befb36090 100644 --- a/test/regress/regress1/sep/sep-02.smt2 +++ b/test/regress/regress1/sep/sep-02.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-03.smt2 b/test/regress/regress1/sep/sep-03.smt2 index f29d081fc..aabdaa100 100644 --- a/test/regress/regress1/sep/sep-03.smt2 +++ b/test/regress/regress1/sep/sep-03.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-fmf-priority.smt2 b/test/regress/regress1/sep/sep-fmf-priority.smt2 index d916a50e5..9b72898cd 100644 --- a/test/regress/regress1/sep/sep-fmf-priority.smt2 +++ b/test/regress/regress1/sep/sep-fmf-priority.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --quant-epr ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort Loc 0) (declare-const l Loc) diff --git a/test/regress/regress1/sep/sep-neg-1refine.smt2 b/test/regress/regress1/sep/sep-neg-1refine.smt2 index 81b107ab5..867d4ccb8 100644 --- a/test/regress/regress1/sep/sep-neg-1refine.smt2 +++ b/test/regress/regress1/sep/sep-neg-1refine.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-nstrict.smt2 b/test/regress/regress1/sep/sep-neg-nstrict.smt2 index 6594a1075..0896d9180 100644 --- a/test/regress/regress1/sep/sep-neg-nstrict.smt2 +++ b/test/regress/regress1/sep/sep-neg-nstrict.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-nstrict2.smt2 b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 index 0243282a3..e66a39f23 100644 --- a/test/regress/regress1/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-simple.smt2 b/test/regress/regress1/sep/sep-neg-simple.smt2 index 8b23a6da8..dc114b0dd 100644 --- a/test/regress/regress1/sep/sep-neg-simple.smt2 +++ b/test/regress/regress1/sep/sep-neg-simple.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-swap.smt2 b/test/regress/regress1/sep/sep-neg-swap.smt2 index ba83f2575..b34e6031f 100644 --- a/test/regress/regress1/sep/sep-neg-swap.smt2 +++ b/test/regress/regress1/sep/sep-neg-swap.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-nterm-again.smt2 b/test/regress/regress1/sep/sep-nterm-again.smt2 index 43fb7b00d..0b38bd189 100644 --- a/test/regress/regress1/sep/sep-nterm-again.smt2 +++ b/test/regress/regress1/sep/sep-nterm-again.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-nterm-val-model.smt2 b/test/regress/regress1/sep/sep-nterm-val-model.smt2 index 635f0895a..34349a5cc 100644 --- a/test/regress/regress1/sep/sep-nterm-val-model.smt2 +++ b/test/regress/regress1/sep/sep-nterm-val-model.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-simp-unc.smt2 b/test/regress/regress1/sep/sep-simp-unc.smt2 index 88950d655..eee6fa211 100644 --- a/test/regress/regress1/sep/sep-simp-unc.smt2 +++ b/test/regress/regress1/sep/sep-simp-unc.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-sort U 0) (declare-heap (U U)) diff --git a/test/regress/regress1/sep/simple-neg-sat.smt2 b/test/regress/regress1/sep/simple-neg-sat.smt2 index 929a8e66f..612776cfa 100644 --- a/test/regress/regress1/sep/simple-neg-sat.smt2 +++ b/test/regress/regress1/sep/simple-neg-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 index 1b7932dc4..c6fa301f0 100644 --- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/split-find-unsat.smt2 b/test/regress/regress1/sep/split-find-unsat.smt2 index ff725f048..346c0083e 100644 --- a/test/regress/regress1/sep/split-find-unsat.smt2 +++ b/test/regress/regress1/sep/split-find-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: unsat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2 index 556be6c18..a07d0b8ae 100644 --- a/test/regress/regress1/sep/wand-0526-sat.smt2 +++ b/test/regress/regress1/sep/wand-0526-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (declare-fun x () Int) (declare-fun y () Int) diff --git a/test/regress/regress1/sep/wand-false.smt2 b/test/regress/regress1/sep/wand-false.smt2 index 9f95c06b7..3d496782c 100644 --- a/test/regress/regress1/sep/wand-false.smt2 +++ b/test/regress/regress1/sep/wand-false.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) (declare-fun x () Int) diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2 index 4ecc8ad1e..47d39eb0b 100644 --- a/test/regress/regress1/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (_ emp Int Int) (pto x 3))) diff --git a/test/regress/regress1/sep/wand-nterm-simp2.smt2 b/test/regress/regress1/sep/wand-nterm-simp2.smt2 index 5b7c92a4a..647421665 100644 --- a/test/regress/regress1/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) (declare-fun x () Int) diff --git a/test/regress/regress1/sep/wand-simp-sat.smt2 b/test/regress/regress1/sep/wand-simp-sat.smt2 index ec63a762e..79c12c028 100644 --- a/test/regress/regress1/sep/wand-simp-sat.smt2 +++ b/test/regress/regress1/sep/wand-simp-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 1))) diff --git a/test/regress/regress1/sep/wand-simp-sat2.smt2 b/test/regress/regress1/sep/wand-simp-sat2.smt2 index 315071c05..76aed570f 100644 --- a/test/regress/regress1/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress1/sep/wand-simp-sat2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) (declare-fun x () Int) diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2 index dabdc18e4..2e90dfb26 100644 --- a/test/regress/regress1/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress1/sep/wand-simp-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: unsat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-fun x () Int) (declare-heap (Int Int)) (assert (wand (pto x 1) (pto x 3))) |