diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-05-07 16:30:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-07 23:30:48 +0000 |
commit | 080f0de4379c4e1fe5a016e40c7852a3abb52760 (patch) | |
tree | bdb25341973ace0bed5d4acfb3517e8cb6dd59fc /test/regress | |
parent | 5bd2fcd60adbfb1f1941d4ed9da6ec10e06dfb12 (diff) |
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).
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 25 | ||||
-rw-r--r-- | test/regress/README.md | 22 | ||||
-rw-r--r-- | test/regress/regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 (renamed from test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/nl/ufnia-factor-open-proof.smt2 (renamed from test/regress/regress1/nl/ufnia-factor-open-proof.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/quantifiers/issue3481-unsat1.smt2 (renamed from test/regress/regress1/quantifiers/issue3481-unsat1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/arith/abz5_1400.smtv1.smt2 (renamed from test/regress/regress2/arith/abz5_1400.smtv1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/error0.smt2 (renamed from test/regress/regress2/error0.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/ho/SYO362^5.p (renamed from test/regress/regress2/ho/SYO362^5.p) | 0 | ||||
-rw-r--r-- | test/regress/regress3/issue4714.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress3/nl/iand-native-1.smt2 (renamed from test/regress/regress1/nl/iand-native-1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 (renamed from test/regress/regress2/quantifiers/ForElimination-scala-9.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/quantifiers/javafe.ast.ArrayInit.35.smt2 (renamed from test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress4/siegel-nl-bases.smt2 (renamed from test/regress/regress3/siegel-nl-bases.smt2) | 0 |
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 |