diff options
| -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 |