diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-25 16:40:24 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-25 16:40:24 -0600 |
commit | ac30758787c01f532774501a06b5cbdc713074dd (patch) | |
tree | d10ed72b89f8fc72ec42e5aba1d1f3cce6a7ede7 /test | |
parent | 6a4b16c643d71c9318042ba7b9d42af71c58ac2f (diff) |
Move slow regressions to regress1 (#5999)
Moves regressions taking >4 seconds (summing all configs) in debug to regress1.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 22 | ||||
-rw-r--r-- | test/regress/regress1/arith/issue3480.smt2 (renamed from test/regress/regress0/arith/issue3480.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/aufbv/fuzz03.smtv1.smt2 (renamed from test/regress/regress0/aufbv/fuzz03.smtv1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bv/fuzz18.smtv1.smt2 (renamed from test/regress/regress0/bv/fuzz18.smtv1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bv/fuzz19.smtv1.smt2 (renamed from test/regress/regress0/bv/fuzz19.smtv1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/decision/bug374a.smtv1.smt2 (renamed from test/regress/regress0/decision/bug374a.smtv1.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/fp/rti_3_5_bug_report.smt2 (renamed from test/regress/regress0/fp/rti_3_5_bug_report.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/nl/ext-rew-aggr-test.smt2 (renamed from test/regress/regress0/nl/ext-rew-aggr-test.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/sygus-inst-nia-psyco-060.smt2 (renamed from test/regress/regress0/quantifiers/sygus-inst-nia-psyco-060.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 (renamed from test/regress/regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/sygus/array-grammar-store.sy (renamed from test/regress/regress0/sygus/array-grammar-store.sy) | 0 | ||||
-rw-r--r-- | test/regress/regress1/uflia/error1.smtv1.smt2 (renamed from test/regress/regress0/uflia/error1.smtv1.smt2) | 0 |
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 |