From ac30758787c01f532774501a06b5cbdc713074dd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 25 Feb 2021 16:40:24 -0600 Subject: [PATCH] Move slow regressions to regress1 (#5999) Moves regressions taking >4 seconds (summing all configs) in debug to regress1. --- test/regress/CMakeLists.txt | 22 +++++++++---------- .../arith/issue3480.smt2 | 0 .../aufbv/fuzz03.smtv1.smt2 | 0 .../bv/fuzz18.smtv1.smt2 | 0 .../bv/fuzz19.smtv1.smt2 | 0 .../decision/bug374a.smtv1.smt2 | 0 .../fp/rti_3_5_bug_report.smt2 | 0 .../nl/ext-rew-aggr-test.smt2 | 0 .../quantifiers/sygus-inst-nia-psyco-060.smt2 | 0 .../sygus-inst-ufnia-sat-t3_rw1505.smt2 | 0 .../sygus/array-grammar-store.sy | 0 .../uflia/error1.smtv1.smt2 | 0 12 files changed, 11 insertions(+), 11 deletions(-) rename test/regress/{regress0 => regress1}/arith/issue3480.smt2 (100%) rename test/regress/{regress0 => regress1}/aufbv/fuzz03.smtv1.smt2 (100%) rename test/regress/{regress0 => regress1}/bv/fuzz18.smtv1.smt2 (100%) rename test/regress/{regress0 => regress1}/bv/fuzz19.smtv1.smt2 (100%) rename test/regress/{regress0 => regress1}/decision/bug374a.smtv1.smt2 (100%) rename test/regress/{regress0 => regress1}/fp/rti_3_5_bug_report.smt2 (100%) rename test/regress/{regress0 => regress1}/nl/ext-rew-aggr-test.smt2 (100%) rename test/regress/{regress0 => regress1}/quantifiers/sygus-inst-nia-psyco-060.smt2 (100%) rename test/regress/{regress0 => regress1}/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 (100%) rename test/regress/{regress0 => regress1}/sygus/array-grammar-store.sy (100%) rename test/regress/{regress0 => regress1}/uflia/error1.smtv1.smt2 (100%) 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 similarity index 100% rename from test/regress/regress0/arith/issue3480.smt2 rename to test/regress/regress1/arith/issue3480.smt2 diff --git a/test/regress/regress0/aufbv/fuzz03.smtv1.smt2 b/test/regress/regress1/aufbv/fuzz03.smtv1.smt2 similarity index 100% rename from test/regress/regress0/aufbv/fuzz03.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/bv/fuzz18.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/bv/fuzz19.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/decision/bug374a.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/fp/rti_3_5_bug_report.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/nl/ext-rew-aggr-test.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/quantifiers/sygus-inst-nia-psyco-060.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/sygus/array-grammar-store.sy rename to 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 similarity index 100% rename from test/regress/regress0/uflia/error1.smtv1.smt2 rename to test/regress/regress1/uflia/error1.smtv1.smt2 -- 2.30.2