Remove redundant logic ALL_SUPPORTED. (#6664)

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)))