12 files changed, 11 insertions, 11 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 37a977371..b08777a51 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -54,7 +54,6 @@ set(regress_0_tests
   regress0/arith/issue1399.smt2
   regress0/arith/issue3412.smt2
   regress0/arith/issue3413.smt2
-  regress0/arith/issue3480.smt2
   regress0/arith/issue3683.smt2
   regress0/arith/issue4367.smt2
   regress0/arith/issue4525.smt2
@@ -127,7 +126,6 @@ set(regress_0_tests
   regress0/aufbv/fuzz02.delta01.smtv1.smt2
   regress0/aufbv/fuzz02.smtv1.smt2
   regress0/aufbv/fuzz03.delta01.smtv1.smt2
-  regress0/aufbv/fuzz03.smtv1.smt2
   regress0/aufbv/fuzz04.delta01.smtv1.smt2
   regress0/aufbv/fuzz04.smtv1.smt2
   regress0/aufbv/fuzz05.delta01.smtv1.smt2
@@ -365,9 +363,7 @@ set(regress_0_tests
   regress0/bv/fuzz18.delta01.smtv1.smt2
   regress0/bv/fuzz18.delta02.smtv1.smt2
   regress0/bv/fuzz18.delta03.smtv1.smt2
-  regress0/bv/fuzz18.smtv1.smt2
   regress0/bv/fuzz19.delta01.smtv1.smt2
-  regress0/bv/fuzz19.smtv1.smt2
   regress0/bv/fuzz20.delta01.smtv1.smt2
   regress0/bv/fuzz20.smtv1.smt2
   regress0/bv/fuzz21.delta01.smtv1.smt2
@@ -516,7 +512,6 @@ set(regress_0_tests
   regress0/decision/bitvec0.smtv1.smt2
   regress0/decision/bitvec5.smtv1.smt2
   regress0/decision/bug347.smtv1.smt2
-  regress0/decision/bug374a.smtv1.smt2
   regress0/decision/bug374b.smt2
   regress0/decision/error122.delta01.smtv1.smt2
   regress0/decision/error122.smtv1.smt2
@@ -578,7 +573,6 @@ set(regress_0_tests
   regress0/fp/issue3536.smt2
   regress0/fp/issue3619.smt2
   regress0/fp/issue4277-assign-func.smt2
-  regress0/fp/rti_3_5_bug_report.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
   regress0/fp/wrong-model.smt2
@@ -671,7 +665,6 @@ set(regress_0_tests
   regress0/named-expr-use.smt2
   regress0/nl/all-logic.smt2
   regress0/nl/coeff-sat.smt2
-  regress0/nl/ext-rew-aggr-test.smt2
   regress0/nl/iand-no-init.smt2
   regress0/nl/issue3003.smt2
   regress0/nl/issue3407.smt2
@@ -891,8 +884,6 @@ set(regress_0_tests
   regress0/quantifiers/selector-trigger.smt2
   regress0/quantifiers/simp-len.smt2
   regress0/quantifiers/simp-typ-test.smt2
-  regress0/quantifiers/sygus-inst-nia-psyco-060.smt2
-  regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
   regress0/quantifiers/ufnia-fv-delta.smt2
   regress0/rec-fun-const-parse-bug.smt2
   regress0/rels/addr_book_0.cvc
@@ -1162,7 +1153,6 @@ set(regress_0_tests
   regress0/strings/unsound-repl-rewrite.smt2
   regress0/sygus/aig-si.sy
   regress0/sygus/array-grammar-select.sy
-  regress0/sygus/array-grammar-store.sy
   regress0/sygus/c100.sy
   regress0/sygus/ccp16.lus.sy
   regress0/sygus/cegqi-si-string-triv-2fun.sy
@@ -1275,7 +1265,6 @@ set(regress_0_tests
   regress0/uflia/diseqprop.05.smtv1.smt2
   regress0/uflia/diseqprop.06.smtv1.smt2
   regress0/uflia/error0.delta01.smtv1.smt2
-  regress0/uflia/error1.smtv1.smt2
   regress0/uflia/error30.smtv1.smt2
   regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2
   regress0/uflia/tiny.smt2
@@ -1405,6 +1394,7 @@ set(regress_1_tests
   regress1/arith/div.06.smt2
   regress1/arith/div.08.smt2
   regress1/arith/div.09.smt2
+  regress1/arith/issue3480.smt2
   regress1/arith/issue3952-rew-eq.smt2
   regress1/arith/issue4985-model-success.smt2
   regress1/arith/issue4985b-model-success.smt2
@@ -1418,6 +1408,7 @@ set(regress_1_tests
   regress1/arrayinuf_error.smt2
   regress1/aufbv/bug348.smtv1.smt2
   regress1/aufbv/bug580.smt2
+  regress1/aufbv/fuzz03.smtv1.smt2
   regress1/aufbv/fuzz10.smtv1.smt2
   regress1/auflia/bug330.smt2
   regress1/boolean-terms-kernel2.smt2
@@ -1461,6 +1452,8 @@ set(regress_1_tests
   regress1/bv/cmu-rdk-3.smt2
   regress1/bv/decision-weight00.smt2
   regress1/bv/divtest.smt2
+  regress1/bv/fuzz18.smtv1.smt2
+  regress1/bv/fuzz19.smtv1.smt2
   regress1/bv/fuzz34.smtv1.smt2
   regress1/bv/fuzz38.smtv1.smt2
   regress1/bv/incorrect1.smtv1.smt2
@@ -1482,10 +1475,12 @@ set(regress_1_tests
   regress1/datatypes/non-simple-rec.smt2
   regress1/datatypes/non-simple-rec-mut-unsat.smt2
   regress1/datatypes/non-simple-rec-param.smt2
+  regress1/decision/bug374a.smtv1.smt2
   regress1/decision/error3.smtv1.smt2
   regress1/decision/quant-Arrays_Q1-noinfer.smt2
   regress1/error.cvc
   regress1/errorcrash.smt2
+  regress1/fp/rti_3_5_bug_report.smt2
   regress1/fmf-fun-dbu.smt2
   regress1/fmf/ALG008-1.smt2
   regress1/fmf/Hoare-z3.931718.smtv1.smt2
@@ -1587,6 +1582,7 @@ set(regress_1_tests
   regress1/nl/exp-soundness-bound.smt2
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
+  regress1/nl/ext-rew-aggr-test.smt2
   regress1/nl/factor_agg_s.smt2
   regress1/nl/iand-native-1.smt2
   regress1/nl/iand-native-2.smt2
@@ -1835,6 +1831,8 @@ set(regress_1_tests
   regress1/quantifiers/smtlibe99bbe.smt2
   regress1/quantifiers/smtlibf957ea.smt2
   regress1/quantifiers/sygus-infer-nested.smt2
+  regress1/quantifiers/sygus-inst-nia-psyco-060.smt2
+  regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
   regress1/quantifiers/symmetric_unsat_7.smt2
   regress1/quantifiers/tpp-unit-fail-qbv.smt2
   regress1/quantifiers/var-eq-trigger.smt2
@@ -2117,6 +2115,7 @@ set(regress_1_tests
   regress1/sygus/abduction_1255.corecstrs.readable.smt2
   regress1/sygus/abduction_streq.readable.smt2
   regress1/sygus/abv.sy
+  regress1/sygus/array-grammar-store.sy
   regress1/sygus/array_search_5-Q-easy.sy
   regress1/sygus/bvudiv-by-2.sy
   regress1/sygus/cegar1.sy
@@ -2274,6 +2273,7 @@ set(regress_1_tests
   regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2
   regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2
   regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2
+  regress1/uflia/error1.smtv1.smt2
   regress1/uflia/microwave21.ec.minimized.smt2
   regress1/uflia/simple_cyclic2.smt2
   regress1/uflia/speed2_e8_449_e8_517.ec.smt2
diff --git a/test/regress/regress0/arith/issue3480.smt2 b/test/regress/regress1/arith/issue3480.smt2
index ef4ad7179..ef4ad7179 100644
--- a/test/regress/regress0/arith/issue3480.smt2
+++ b/test/regress/regress1/arith/issue3480.smt2
diff --git a/test/regress/regress0/aufbv/fuzz03.smtv1.smt2 b/test/regress/regress1/aufbv/fuzz03.smtv1.smt2
index 919e86fbf..919e86fbf 100644
--- a/test/regress/regress0/aufbv/fuzz03.smtv1.smt2
+++ b/test/regress/regress1/aufbv/fuzz03.smtv1.smt2
diff --git a/test/regress/regress0/bv/fuzz18.smtv1.smt2 b/test/regress/regress1/bv/fuzz18.smtv1.smt2
index 4a57338a1..4a57338a1 100644
--- a/test/regress/regress0/bv/fuzz18.smtv1.smt2
+++ b/test/regress/regress1/bv/fuzz18.smtv1.smt2
diff --git a/test/regress/regress0/bv/fuzz19.smtv1.smt2 b/test/regress/regress1/bv/fuzz19.smtv1.smt2
index bafa631e0..bafa631e0 100644
--- a/test/regress/regress0/bv/fuzz19.smtv1.smt2
+++ b/test/regress/regress1/bv/fuzz19.smtv1.smt2
diff --git a/test/regress/regress0/decision/bug374a.smtv1.smt2 b/test/regress/regress1/decision/bug374a.smtv1.smt2
index 9e64c56f3..9e64c56f3 100644
--- a/test/regress/regress0/decision/bug374a.smtv1.smt2
+++ b/test/regress/regress1/decision/bug374a.smtv1.smt2
diff --git a/test/regress/regress0/fp/rti_3_5_bug_report.smt2 b/test/regress/regress1/fp/rti_3_5_bug_report.smt2
index 5a52ffcc9..5a52ffcc9 100644
--- a/test/regress/regress0/fp/rti_3_5_bug_report.smt2
+++ b/test/regress/regress1/fp/rti_3_5_bug_report.smt2
diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress1/nl/ext-rew-aggr-test.smt2
index c540ecbe5..c540ecbe5 100644
--- a/test/regress/regress0/nl/ext-rew-aggr-test.smt2
+++ b/test/regress/regress1/nl/ext-rew-aggr-test.smt2
diff --git a/test/regress/regress0/quantifiers/sygus-inst-nia-psyco-060.smt2 b/test/regress/regress1/quantifiers/sygus-inst-nia-psyco-060.smt2
index 45fc5d916..45fc5d916 100644
--- a/test/regress/regress0/quantifiers/sygus-inst-nia-psyco-060.smt2
+++ b/test/regress/regress1/quantifiers/sygus-inst-nia-psyco-060.smt2
diff --git a/test/regress/regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 b/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
index 1dae93eb5..1dae93eb5 100644
--- a/test/regress/regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
+++ b/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
diff --git a/test/regress/regress0/sygus/array-grammar-store.sy b/test/regress/regress1/sygus/array-grammar-store.sy
index 025a17b15..025a17b15 100644
--- a/test/regress/regress0/sygus/array-grammar-store.sy
+++ b/test/regress/regress1/sygus/array-grammar-store.sy
diff --git a/test/regress/regress0/uflia/error1.smtv1.smt2 b/test/regress/regress1/uflia/error1.smtv1.smt2
index a652ad707..a652ad707 100644
--- a/test/regress/regress0/uflia/error1.smtv1.smt2
+++ b/test/regress/regress1/uflia/error1.smtv1.smt2