Move slow regressions and update guidelines. (#6508)

This moves regression test that exceed the time limit of their
respective level to the appropriate level. It further updates the
guidelines in the README with information on how to properly categorize
regression tests into levels (with time limits).

Note: Test regress3/issue4717.smt2 was previously unsolved (unknown) and
      is now sat (Z3 agrees).

13 files changed, 31 insertions, 18 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a64a1eb1e..9bda5cff1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1576,7 +1576,6 @@ set(regress_1_tests
   regress1/issue5739-rtf-processed.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
-  regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
   regress1/model-blocker-simple.smt2
   regress1/model-blocker-values.smt2
   regress1/nl/approx-sqrt.smt2
@@ -1599,7 +1598,6 @@ set(regress_1_tests
   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
   regress1/nl/iand-native-granularities.smt2
   regress1/nl/issue3300-approx-sqrt-witness.smt2
@@ -1647,7 +1645,6 @@ set(regress_1_tests
   regress1/nl/sugar-ident-3.smt2
   regress1/nl/sugar-ident.smt2
   regress1/nl/tan-rewrite2.smt2
-  regress1/nl/ufnia-factor-open-proof.smt2
   regress1/nl/zero-subset.smt2
   regress1/non-fatal-errors.smt2
   regress1/parsing_ringer.cvc
@@ -1763,7 +1760,6 @@ set(regress_1_tests
   regress1/quantifiers/issue3316.smt2
   regress1/quantifiers/issue3317.smt2
   regress1/quantifiers/issue3481.smt2
-  regress1/quantifiers/issue3481-unsat1.smt2
   regress1/quantifiers/issue3537.smt2
   regress1/quantifiers/issue3628.smt2
   regress1/quantifiers/issue3664.smt2
@@ -2337,7 +2333,6 @@ set(regress_2_tests
   regress2/DTP_k2_n35_c175_s15.smt2
   regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
   regress2/GEO123+1.minimized.smt2
-  regress2/arith/abz5_1400.smtv1.smt2
   regress2/arith/arith-int-098.cvc
   regress2/arith/pursuit-safety-11.smtv1.smt2
   regress2/arith/pursuit-safety-12.smtv1.smt2
@@ -2365,7 +2360,6 @@ set(regress_2_tests
   regress2/bv_to_int_mask_array_2.smt2
   regress2/bv_to_int_mask_array_3.smt2
   regress2/bv_to_int_shifts.smt2
-  regress2/error0.smt2
   regress2/error1.smtv1.smt2
   regress2/fuzz_2.smtv1.smt2
   regress2/hash_sat_06_19.smt2
@@ -2377,24 +2371,24 @@ set(regress_2_tests
   regress2/ho/fta0409.smt2
   regress2/ho/involved_parsing_ALG248^3.p
   regress2/ho/partial_app_interpreted_SWW474^2.p
-  regress2/ho/SYO362^5.p
   regress2/hole7.cvc
   regress2/hole8.cvc
   regress2/instance_1444.smtv1.smt2
   regress2/issue3687-check-models.smt2
   regress2/issue4707-bv-to-bool-large.smt2
   regress2/issue6495-dup-pat-term.smt2
+  regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
   regress2/nl/nt-lemmas-bad.smt2
+  regress2/nl/ufnia-factor-open-proof.smt2
   regress2/ooo.rf6.smt2
   regress2/ooo.tag10.smt2
   regress2/piVC_5581bd.smt2
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
-  regress2/quantifiers/ForElimination-scala-9.smt2
   regress2/quantifiers/gn-wrong-091018.smt2
-  regress2/quantifiers/javafe.ast.ArrayInit.35.smt2
+  regress2/quantifiers/issue3481-unsat1.smt2
   regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
   regress2/quantifiers/javafe.ast.WhileStmt.447.smt2
   regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2
@@ -2452,6 +2446,7 @@ set(regress_2_tests
 # Regression level 3 tests
 
 set(regress_3_tests
+  regress3/arith/abz5_1400.smtv1.smt2
   regress3/arith_prp-13-24.smt2
   regress3/aufbv-wchains010ue.smtv1.smt2
   regress3/auflia-fuzz06.smtv1.smt2
@@ -2477,24 +2472,27 @@ set(regress_3_tests
   regress3/decision-wchains010ue.smtv1.smt2
   regress3/DRAGON_1.lus.sy
   regress3/eq_diamond14.smtv1.smt2
+  regress3/error0.smt2
   regress3/friedman_n4_i5.smtv1.smt2
   regress3/friedman_n6_i4.smtv1.smt2
+  regress3/ho/SYO362^5.p
   regress3/hole9.cvc
   regress3/hole10.cvc
   regress3/incorrect1.smtv1.smt2
   regress3/interpol2.smt2
   regress3/inv_gen_n_c11.sy
   regress3/issue4170.smt2
-  regress3/issue4476-ext-rew.smt2
   regress3/issue4714.smt2
   regress3/lpsat-goal-9.smt2
   regress3/nia-max-square.sy
+  regress3/nl/iand-native-1.smt2
   regress3/PEQ018_size4.smtv1.smt2
   regress3/policyM.sy
+  regress3/quantifiers/ForElimination-scala-9.smt2
+  regress3/quantifiers/javafe.ast.ArrayInit.35.smt2
   regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
   regress3/regex-rrv.sy
-  regress3/siegel-nl-bases.smt2
   regress3/sixfuncs.sy
   regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
   regress3/strings-any-term.sy
@@ -2502,7 +2500,6 @@ set(regress_3_tests
   regress3/strings/norn-dis-0707-3.smt2
   regress3/strings/replace_re_all.smt2
   regress3/unbdd_inv_gen_ex7.sy
-  regress3/unifpi-solve-car_1.lus.sy
   regress3/vcb.sy
 )
 
@@ -2523,6 +2520,7 @@ set(regress_4_tests
   regress4/NEQ016_size5.smtv1.smt2
   regress4/pp-regfile.smtv1.smt2
   regress4/sets-card-neg-mem-union-2.smt2
+  regress4/siegel-nl-bases.smt2
   regress4/unsat-circ-reduce.smt2
   regress4/xs-11-20-5-2-5-3.smt2
   regress4/xs-11-20-5-2-5-3.smtv1.smt2
@@ -2616,6 +2614,9 @@ set(regression_disabled_tests
   regress1/sygus/issue3498.smt2
   regress2/arith/miplib-opt1217--27.smt2
   regress2/nl/dumortier-050317.smt2
+  # time out
+  regress3/unifpi-solve-car_1.lus.sy
+  regress3/issue4476-ext-rew.smt2
 )
 
 #-----------------------------------------------------------------------------#
diff --git a/test/regress/README.md b/test/regress/README.md
index f7fb2b6d3..efd79472b 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -1,12 +1,24 @@
 # Regression
 
-## Regression Levels and Running Regression Tests
+## Regression Levels
 
-cvc5's regression tests are divided into 5 levels (level 0 to 4). Higher
-regression levels are reserved for longer running regressions. 
+cvc5's regression tests are divided into 5 levels (level 0 to 4), based on
+their run time (`production` build with `--assertions`).
+Higher regression levels are reserved for longer running regressions.
 
-For running regressions tests, 
-see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file.
+The time limits for each level are:
+
+* **Level 0:** <= 1s
+* **Level 1:** <= 5s
+* **Level 2:** <= 10s
+* **Level 3:** <= 100s
+* **Level 4:** > 100s
+
+## Running Regression Tests
+
+For running regressions tests, see the
+[INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4)
+file.
 
 By default, each invocation of cvc5 is done with a 10 minute timeout. To use a
 different timeout, set the `TEST_TIMEOUT` environment variable:
diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 b/test/regress/regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
index 038b63019..038b63019 100644
--- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
+++ b/test/regress/regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
diff --git a/test/regress/regress1/nl/ufnia-factor-open-proof.smt2 b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2
index bcb077f4f..bcb077f4f 100644
--- a/test/regress/regress1/nl/ufnia-factor-open-proof.smt2
+++ b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2
diff --git a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 b/test/regress/regress2/quantifiers/issue3481-unsat1.smt2
index 9cf535dc7..9cf535dc7 100644
--- a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
+++ b/test/regress/regress2/quantifiers/issue3481-unsat1.smt2
diff --git a/test/regress/regress2/arith/abz5_1400.smtv1.smt2 b/test/regress/regress3/arith/abz5_1400.smtv1.smt2
index 09ac46936..09ac46936 100644
--- a/test/regress/regress2/arith/abz5_1400.smtv1.smt2
+++ b/test/regress/regress3/arith/abz5_1400.smtv1.smt2
diff --git a/test/regress/regress2/error0.smt2 b/test/regress/regress3/error0.smt2
index 73177a252..73177a252 100644
--- a/test/regress/regress2/error0.smt2
+++ b/test/regress/regress3/error0.smt2
diff --git a/test/regress/regress2/ho/SYO362^5.p b/test/regress/regress3/ho/SYO362^5.p
index c01d3f235..c01d3f235 100644
--- a/test/regress/regress2/ho/SYO362^5.p
+++ b/test/regress/regress3/ho/SYO362^5.p
diff --git a/test/regress/regress3/issue4714.smt2 b/test/regress/regress3/issue4714.smt2
index ee3e59a32..ac8914044 100644
--- a/test/regress/regress3/issue4714.smt2
+++ b/test/regress/regress3/issue4714.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --check-models
-; EXPECT: unknown
+; EXPECT: sat 
 (set-logic UFNIRA)
 (declare-fun c (Int) Int)
 (define-fun d ((k Int)) Int (- (c k) 10))
diff --git a/test/regress/regress1/nl/iand-native-1.smt2 b/test/regress/regress3/nl/iand-native-1.smt2
index 0835b7066..0835b7066 100644
--- a/test/regress/regress1/nl/iand-native-1.smt2
+++ b/test/regress/regress3/nl/iand-native-1.smt2
diff --git a/test/regress/regress2/quantifiers/ForElimination-scala-9.smt2 b/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2
index 04ea50b72..04ea50b72 100644
--- a/test/regress/regress2/quantifiers/ForElimination-scala-9.smt2
+++ b/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2
diff --git a/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 b/test/regress/regress3/quantifiers/javafe.ast.ArrayInit.35.smt2
index dcdc41886..dcdc41886 100644
--- a/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2
+++ b/test/regress/regress3/quantifiers/javafe.ast.ArrayInit.35.smt2
diff --git a/test/regress/regress3/siegel-nl-bases.smt2 b/test/regress/regress4/siegel-nl-bases.smt2
index cf6e3ab5e..cf6e3ab5e 100644
--- a/test/regress/regress3/siegel-nl-bases.smt2
+++ b/test/regress/regress4/siegel-nl-bases.smt2