From 01d6e3933a3d733d3c1b5486ce1df8389cd6a176 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 21 Oct 2016 14:01:17 -0500 Subject: [PATCH] Move slow regress0 benchmarks to regress1, increment regress1 through regress3. --- test/regress/regress0/Makefile.am | 3 -- test/regress/regress0/aufbv/Makefile.am | 1 - test/regress/regress0/auflia/Makefile.am | 1 - test/regress/regress0/bv/Makefile.am | 5 +- test/regress/regress0/datatypes/Makefile.am | 1 - test/regress/regress0/decision/Makefile.am | 1 - test/regress/regress0/fmf/Makefile.am | 1 - test/regress/regress0/lemmas/Makefile.am | 5 +- .../regress/regress0/rewriterules/Makefile.am | 4 +- test/regress/regress0/sep/Makefile.am | 4 -- test/regress/regress0/sets/Makefile.am | 4 +- test/regress/regress0/strings/Makefile.am | 2 - test/regress/regress0/sygus/Makefile.am | 3 +- test/regress/regress1/Makefile.am | 50 +++---------------- .../{regress0 => regress1}/aufbv/fuzz10.smt | 0 .../{regress0 => regress1}/auflia/bug330.smt2 | 0 .../regress/{regress0 => regress1}/bug425.cvc | 0 .../{regress0 => regress1}/bug519.smt2 | 0 .../{regress0 => regress1}/bug521.smt2 | 0 .../{regress0 => regress1}/bv/bv-proof00.smt | 0 .../{regress0 => regress1}/bv/fuzz34.smt | 0 .../{regress0 => regress1}/bv/fuzz38.smt | 0 .../datatypes/manos-model.smt2 | 0 .../decision/error3.smt | 0 .../fmf/ForElimination-scala-9.smt2 | 0 .../clocksynchro_5clocks.main_invar.base.smt | 0 .../lemmas/pursuit-safety-8.smt | 0 .../simple_startup_9nodes.abstract.base.smt | 0 .../reachability_back_to_the_future.smt2 | 0 .../rewriterules/read5.smt2 | 0 .../{regress0 => regress1}/sep/loop-1220.smt2 | 0 .../sep/sep-simp-unc.smt2 | 0 .../sep/split-find-unsat-w-emp.smt2 | 0 .../sep/split-find-unsat.smt2 | 0 .../sets/card-vc6-minimized.smt2 | 0 .../sets/sets-disequal.smt2 | 0 .../strings/cmu-5042-0707-2.smt2 | 0 .../strings/cmu-dis-0707-3.smt2 | 0 .../{regress0 => regress1}/sygus/hd-sdiv.sy | 0 .../DTP_k2_n35_c175_s15.smt2 | 0 ...IREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 | 0 ...3_e2_2236_e7_3681.ec.minimized.smt2.expect | 0 .../GEO123+1.minimized.smt2 | 0 test/regress/regress2/Makefile | 2 +- test/regress/regress2/Makefile.am | 46 +++++++++++------ .../{regress1 => regress2}/arith/Makefile | 0 .../{regress1 => regress2}/arith/Makefile.am | 0 .../arith/abz5_1400.smt | 0 .../arith/lpsat-goal-9.smt2 | 0 .../arith/prp-13-24.smt2 | 0 .../arith/pursuit-safety-11.smt | 0 .../arith/pursuit-safety-12.smt | 0 .../arith/qlock-4-10-9.base.cvc.smt2 | 0 .../arith/sc-7.base.cvc.smt | 0 .../arith/uart-8.base.cvc.smt | 0 .../{regress1 => regress2}/auflia-fuzz06.smt | 0 .../regress/{regress1 => regress2}/bug136.smt | 0 .../regress/{regress1 => regress2}/bug148.smt | 0 .../{regress1 => regress2}/bug394.smt2 | 0 .../{regress1 => regress2}/error0.smt2 | 0 .../regress/{regress1 => regress2}/error1.smt | 0 .../{regress1 => regress2}/friedman_n4_i5.smt | 0 .../regress/{regress1 => regress2}/fuzz_2.smt | 0 .../hash_sat_06_19.smt2 | 0 .../hash_sat_07_17.smt2 | 0 .../hash_sat_09_09.smt2 | 0 .../hash_sat_10_09.smt2 | 0 test/regress/{regress1 => regress2}/hole7.cvc | 0 test/regress/{regress1 => regress2}/hole8.cvc | 0 .../{regress1 => regress2}/instance_1444.smt | 0 .../{regress1 => regress2}/ooo.rf6.smt2 | 0 .../{regress1 => regress2}/ooo.tag10.smt2 | 0 .../{regress1 => regress2}/piVC_5581bd.smt2 | 0 .../typed_v1l50016-simp.cvc | 0 .../{regress1 => regress2}/uflia-error0.smt2 | 0 .../uflia-error0.smt2.expect | 0 .../xs-09-16-3-4-1-5.decn.smt | 0 .../xs-09-16-3-4-1-5.decn.smt.expect | 0 .../xs-09-16-3-4-1-5.smt | 0 .../xs-11-20-5-2-5-3.smt | 0 .../xs-11-20-5-2-5-3.smt2 | 0 test/regress/regress3/Makefile | 2 +- test/regress/regress3/Makefile.am | 27 ++++++---- .../{regress2 => regress3}/bmc-ibm-1.smt | 0 .../{regress2 => regress3}/bmc-ibm-2.smt | 0 .../{regress2 => regress3}/bmc-ibm-5.smt | 0 .../{regress2 => regress3}/bmc-ibm-7.smt | 0 .../regress/{regress2 => regress3}/bug497.cvc | 0 .../{regress2 => regress3}/eq_diamond14.smt | 0 .../{regress2 => regress3}/friedman_n6_i4.smt | 0 test/regress/{regress2 => regress3}/hole9.cvc | 0 .../{regress2 => regress3}/incorrect1.smt | 0 .../{regress2 => regress3}/incorrect2.smt | 0 .../{regress2 => regress3}/pp-regfile.smt | 0 .../pp-regfile.smt.expect | 0 .../qwh.35.405.shuffled-as.sat03-1651.smt | 0 .../C880mul.miter.shuffled-as.sat03-348.smt | 0 test/regress/{regress1 => regress4}/Makefile | 2 +- test/regress/regress4/Makefile.am | 48 ++++++++++++++++++ .../{regress3 => regress4}/NEQ016_size5.smt | 0 .../regress/{regress3 => regress4}/bug143.smt | 0 .../comb2.shuffled-as.sat03-420.smt | 0 .../regress/{regress3 => regress4}/hole10.cvc | 0 .../{regress3 => regress4}/instance_1151.smt | 0 104 files changed, 111 insertions(+), 101 deletions(-) rename test/regress/{regress0 => regress1}/aufbv/fuzz10.smt (100%) rename test/regress/{regress0 => regress1}/auflia/bug330.smt2 (100%) rename test/regress/{regress0 => regress1}/bug425.cvc (100%) rename test/regress/{regress0 => regress1}/bug519.smt2 (100%) rename test/regress/{regress0 => regress1}/bug521.smt2 (100%) rename test/regress/{regress0 => regress1}/bv/bv-proof00.smt (100%) rename test/regress/{regress0 => regress1}/bv/fuzz34.smt (100%) rename test/regress/{regress0 => regress1}/bv/fuzz38.smt (100%) rename test/regress/{regress0 => regress1}/datatypes/manos-model.smt2 (100%) rename test/regress/{regress0 => regress1}/decision/error3.smt (100%) rename test/regress/{regress0 => regress1}/fmf/ForElimination-scala-9.smt2 (100%) rename test/regress/{regress0 => regress1}/lemmas/clocksynchro_5clocks.main_invar.base.smt (100%) rename test/regress/{regress0 => regress1}/lemmas/pursuit-safety-8.smt (100%) rename test/regress/{regress0 => regress1}/lemmas/simple_startup_9nodes.abstract.base.smt (100%) rename test/regress/{regress0 => regress1}/rewriterules/reachability_back_to_the_future.smt2 (100%) rename test/regress/{regress0 => regress1}/rewriterules/read5.smt2 (100%) rename test/regress/{regress0 => regress1}/sep/loop-1220.smt2 (100%) rename test/regress/{regress0 => regress1}/sep/sep-simp-unc.smt2 (100%) rename test/regress/{regress0 => regress1}/sep/split-find-unsat-w-emp.smt2 (100%) rename test/regress/{regress0 => regress1}/sep/split-find-unsat.smt2 (100%) rename test/regress/{regress0 => regress1}/sets/card-vc6-minimized.smt2 (100%) rename test/regress/{regress0 => regress1}/sets/sets-disequal.smt2 (100%) rename test/regress/{regress0 => regress1}/strings/cmu-5042-0707-2.smt2 (100%) rename test/regress/{regress0 => regress1}/strings/cmu-dis-0707-3.smt2 (100%) rename test/regress/{regress0 => regress1}/sygus/hd-sdiv.sy (100%) rename test/regress/{regress1 => regress2}/DTP_k2_n35_c175_s15.smt2 (100%) rename test/regress/{regress1 => regress2}/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 (100%) rename test/regress/{regress1 => regress2}/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect (100%) rename test/regress/{regress1 => regress2}/GEO123+1.minimized.smt2 (100%) rename test/regress/{regress1 => regress2}/arith/Makefile (100%) rename test/regress/{regress1 => regress2}/arith/Makefile.am (100%) rename test/regress/{regress1 => regress2}/arith/abz5_1400.smt (100%) rename test/regress/{regress1 => regress2}/arith/lpsat-goal-9.smt2 (100%) rename test/regress/{regress1 => regress2}/arith/prp-13-24.smt2 (100%) rename test/regress/{regress1 => regress2}/arith/pursuit-safety-11.smt (100%) rename test/regress/{regress1 => regress2}/arith/pursuit-safety-12.smt (100%) rename test/regress/{regress1 => regress2}/arith/qlock-4-10-9.base.cvc.smt2 (100%) rename test/regress/{regress1 => regress2}/arith/sc-7.base.cvc.smt (100%) rename test/regress/{regress1 => regress2}/arith/uart-8.base.cvc.smt (100%) rename test/regress/{regress1 => regress2}/auflia-fuzz06.smt (100%) rename test/regress/{regress1 => regress2}/bug136.smt (100%) rename test/regress/{regress1 => regress2}/bug148.smt (100%) rename test/regress/{regress1 => regress2}/bug394.smt2 (100%) rename test/regress/{regress1 => regress2}/error0.smt2 (100%) rename test/regress/{regress1 => regress2}/error1.smt (100%) rename test/regress/{regress1 => regress2}/friedman_n4_i5.smt (100%) rename test/regress/{regress1 => regress2}/fuzz_2.smt (100%) rename test/regress/{regress1 => regress2}/hash_sat_06_19.smt2 (100%) rename test/regress/{regress1 => regress2}/hash_sat_07_17.smt2 (100%) rename test/regress/{regress1 => regress2}/hash_sat_09_09.smt2 (100%) rename test/regress/{regress1 => regress2}/hash_sat_10_09.smt2 (100%) rename test/regress/{regress1 => regress2}/hole7.cvc (100%) rename test/regress/{regress1 => regress2}/hole8.cvc (100%) rename test/regress/{regress1 => regress2}/instance_1444.smt (100%) rename test/regress/{regress1 => regress2}/ooo.rf6.smt2 (100%) rename test/regress/{regress1 => regress2}/ooo.tag10.smt2 (100%) rename test/regress/{regress1 => regress2}/piVC_5581bd.smt2 (100%) rename test/regress/{regress1 => regress2}/typed_v1l50016-simp.cvc (100%) rename test/regress/{regress1 => regress2}/uflia-error0.smt2 (100%) rename test/regress/{regress1 => regress2}/uflia-error0.smt2.expect (100%) rename test/regress/{regress1 => regress2}/xs-09-16-3-4-1-5.decn.smt (100%) rename test/regress/{regress1 => regress2}/xs-09-16-3-4-1-5.decn.smt.expect (100%) rename test/regress/{regress1 => regress2}/xs-09-16-3-4-1-5.smt (100%) rename test/regress/{regress1 => regress2}/xs-11-20-5-2-5-3.smt (100%) rename test/regress/{regress1 => regress2}/xs-11-20-5-2-5-3.smt2 (100%) rename test/regress/{regress2 => regress3}/bmc-ibm-1.smt (100%) rename test/regress/{regress2 => regress3}/bmc-ibm-2.smt (100%) rename test/regress/{regress2 => regress3}/bmc-ibm-5.smt (100%) rename test/regress/{regress2 => regress3}/bmc-ibm-7.smt (100%) rename test/regress/{regress2 => regress3}/bug497.cvc (100%) rename test/regress/{regress2 => regress3}/eq_diamond14.smt (100%) rename test/regress/{regress2 => regress3}/friedman_n6_i4.smt (100%) rename test/regress/{regress2 => regress3}/hole9.cvc (100%) rename test/regress/{regress2 => regress3}/incorrect1.smt (100%) rename test/regress/{regress2 => regress3}/incorrect2.smt (100%) rename test/regress/{regress2 => regress3}/pp-regfile.smt (100%) rename test/regress/{regress2 => regress3}/pp-regfile.smt.expect (100%) rename test/regress/{regress2 => regress3}/qwh.35.405.shuffled-as.sat03-1651.smt (100%) rename test/regress/{regress3 => regress4}/C880mul.miter.shuffled-as.sat03-348.smt (100%) rename test/regress/{regress1 => regress4}/Makefile (76%) create mode 100644 test/regress/regress4/Makefile.am rename test/regress/{regress3 => regress4}/NEQ016_size5.smt (100%) rename test/regress/{regress3 => regress4}/bug143.smt (100%) rename test/regress/{regress3 => regress4}/comb2.shuffled-as.sat03-420.smt (100%) rename test/regress/{regress3 => regress4}/hole10.cvc (100%) rename test/regress/{regress3 => regress4}/instance_1151.smt (100%) diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 45842065f..c790165ef 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -147,16 +147,13 @@ BUG_TESTS = \ bug398.smt2 \ bug421.smt2 \ bug421b.smt2 \ - bug425.cvc \ bug480.smt2 \ bug484.smt2 \ bug486.cvc \ bug507.smt2 \ bug512.minimized.smt2 \ bug516.smt2 \ - bug519.smt2 \ bug520.smt2 \ - bug521.smt2 \ bug521.minimized.smt2 \ bug522.smt2 \ bug528a.smt2 \ diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 38705c22a..d88128e72 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -48,7 +48,6 @@ TESTS = \ fuzz07.smt \ fuzz08.smt \ fuzz09.smt \ - fuzz10.smt \ fuzz11.smt \ fuzz12.smt \ fuzz13.smt \ diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index d182539bc..82ea731d4 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -19,7 +19,6 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - bug330.smt2 \ bug336.smt2 \ fuzz01.delta01.smt \ fuzz02.smt \ diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index d85b3d109..0b99024eb 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -78,7 +78,6 @@ SMT_TESTS = \ fuzz33.delta01.smt \ fuzz33.smt \ fuzz34.delta01.smt \ - fuzz34.smt \ fuzz35.delta01.smt \ fuzz35.smt \ fuzz36.delta01.smt \ @@ -86,7 +85,6 @@ SMT_TESTS = \ fuzz37.delta01.smt \ fuzz37.smt \ fuzz38.delta01.smt \ - fuzz38.smt \ fuzz39.delta01.smt \ fuzz39.smt \ fuzz40.delta01.smt \ @@ -95,8 +93,7 @@ SMT_TESTS = \ calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \ smtcompbug.smt \ unsound1.smt2 \ - unsound1-reduced.smt2 \ - bv-proof00.smt + unsound1-reduced.smt2 # Regression tests for SMT2 inputs SMT2_TESTS = divtest.smt2 diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 350a948aa..c177129b4 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -64,7 +64,6 @@ TESTS = \ cdt-non-canon-stream.smt2 \ stream-singleton.smt2 \ is_test.smt2 \ - manos-model.smt2 \ bug625.smt2 \ cdt-model-cade15.smt2 \ sc-cdt1.smt2 \ diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 90a18f0e2..6aea21f3f 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -34,7 +34,6 @@ TESTS = \ error20.delta01.smt \ error122.smt \ error122.delta01.smt \ - error3.smt \ error3.delta01.smt \ pp-regfile.delta01.smt \ pp-regfile.delta02.smt diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index b7daadfd1..c10b3c668 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -53,7 +53,6 @@ TESTS = \ nun-0208-to.smt2 \ datatypes-ufinite.smt2 \ datatypes-ufinite-nested.smt2 \ - ForElimination-scala-9.smt2 \ agree466.smt2 \ LeftistHeap.scala-8-ncm.smt2 \ sc-crash-052316.smt2 \ diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am index 9ede6d4c0..26610304a 100644 --- a/test/regress/regress0/lemmas/Makefile.am +++ b/test/regress/regress0/lemmas/Makefile.am @@ -25,11 +25,8 @@ MAKEFLAGS = -k SMT_TESTS = \ clocksynchro_5clocks.main_invar.base.model.smt \ sc_init_frame_gap.induction.smt \ - clocksynchro_5clocks.main_invar.base.smt \ mode_cntrl.induction.smt \ - fs_not_sc_seen.induction.smt \ - pursuit-safety-8.smt \ - simple_startup_9nodes.abstract.base.smt + fs_not_sc_seen.induction.smt TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 31f99905c..3224563ab 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -26,11 +26,9 @@ TESTS = \ length_gen_020.smt2 \ datatypes.smt2 \ datatypes_sat.smt2 \ - reachability_back_to_the_future.smt2 \ relation.smt2 \ simulate_rewriting.smt2 \ - native_arrays.smt2 \ - read5.smt2 + native_arrays.smt2 # length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index b43a9a570..d7bfa2d57 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -33,20 +33,16 @@ TESTS = \ nspatial-simp.smt2 \ sep-neg-1refine.smt2 \ sep-neg-simple.smt2 \ - sep-simp-unc.smt2 \ sep-simp-unsat-emp.smt2 \ simple-neg-sat.smt2 \ wand-simp-sat.smt2 \ wand-simp-sat2.smt2 \ wand-simp-unsat.smt2 \ sep-nterm-again.smt2 \ - split-find-unsat.smt2 \ - split-find-unsat-w-emp.smt2 \ nemp.smt2 \ wand-crash.smt2 \ wand-nterm-simp.smt2 \ wand-nterm-simp2.smt2 \ - loop-1220.smt2 \ chain-int.smt2 \ sep-neg-swap.smt2 \ sep-neg-nstrict2.smt2 \ diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 2f36cc188..9c970c45a 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -50,7 +50,6 @@ TESTS = \ fuzz15201.smt2 \ fuzz31811.smt2 \ rec_copy_loop_check_heap_access_43_4.smt2 \ - sets-disequal.smt2 \ sets-equal.smt2 \ sets-inter.smt2 \ sets-sample.smt2 \ @@ -64,8 +63,7 @@ TESTS = \ union-1b.smt2 \ union-2.smt2 \ dt-simp-mem.smt2 \ - card3-ground.smt2 \ - card-vc6-minimized.smt2 + card3-ground.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 2e4fd4e1c..88f3763e1 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -79,8 +79,6 @@ TESTS = \ cmu-2db2-extf-reg.smt2 \ norn-nel-bug-052116.smt2 \ cmu-disagree-0707-dd.smt2 \ - cmu-5042-0707-2.smt2 \ - cmu-dis-0707-3.smt2 \ nf-ff-contains-abs.smt2 \ csp-prefix-exp-bug.smt2 \ cmu-substr-rw.smt2 \ diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index b503a65b8..695c52cc6 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -50,8 +50,7 @@ TESTS = commutative.sy \ no-mention.sy \ max2-univ.sy \ strings-small.sy \ - strings-unconstrained.sy \ - hd-sdiv.sy + strings-unconstrained.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 5f292b893..c399a797f 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith +SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf strings sets sygus sep # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) @@ -20,50 +20,16 @@ MAKEFLAGS = -k # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" -TESTS = bug136.smt \ - bug148.smt \ - bug394.smt2 \ - DTP_k2_n35_c175_s15.smt2 \ - GEO123+1.minimized.smt2 \ - error1.smt \ - friedman_n4_i5.smt \ - hole7.cvc \ - hole8.cvc \ - instance_1444.smt \ - fuzz_2.smt \ - hash_sat_10_09.smt2 \ - hash_sat_07_17.smt2 \ - ooo.tag10.smt2 \ - hash_sat_06_19.smt2 \ - hash_sat_09_09.smt2 \ - ooo.rf6.smt2 \ - auflia-fuzz06.smt \ - piVC_5581bd.smt2 \ - typed_v1l50016-simp.cvc \ - FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ - xs-09-16-3-4-1-5.smt \ - xs-09-16-3-4-1-5.decn.smt \ - uflia-error0.smt2 - -EXTRA_DIST = $(TESTS) \ - FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ - uflia-error0.smt2.expect \ - xs-09-16-3-4-1-5.decn.smt.expect - -#if CVC4_BUILD_PROFILE_COMPETITION -#else -#TESTS += \ -# error.cvc -#endif -# -# and make sure to distribute it -#EXTRA_DIST += \ -# error.cvc +TESTS = bug425.cvc \ + bug519.smt2 \ + bug521.smt2 + +EXTRA_DIST = $(TESTS) # synonyms for "check" in this directory .PHONY: regress regress1 test regress regress1 test: check # do nothing in this subdir -.PHONY: regress0 regress2 regress3 -regress0 regress2 regress3: +.PHONY: regress0 regress2 regress3 regress4 +regress0 regress2 regress3 regress4: diff --git a/test/regress/regress0/aufbv/fuzz10.smt b/test/regress/regress1/aufbv/fuzz10.smt similarity index 100% rename from test/regress/regress0/aufbv/fuzz10.smt rename to test/regress/regress1/aufbv/fuzz10.smt diff --git a/test/regress/regress0/auflia/bug330.smt2 b/test/regress/regress1/auflia/bug330.smt2 similarity index 100% rename from test/regress/regress0/auflia/bug330.smt2 rename to test/regress/regress1/auflia/bug330.smt2 diff --git a/test/regress/regress0/bug425.cvc b/test/regress/regress1/bug425.cvc similarity index 100% rename from test/regress/regress0/bug425.cvc rename to test/regress/regress1/bug425.cvc diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress1/bug519.smt2 similarity index 100% rename from test/regress/regress0/bug519.smt2 rename to test/regress/regress1/bug519.smt2 diff --git a/test/regress/regress0/bug521.smt2 b/test/regress/regress1/bug521.smt2 similarity index 100% rename from test/regress/regress0/bug521.smt2 rename to test/regress/regress1/bug521.smt2 diff --git a/test/regress/regress0/bv/bv-proof00.smt b/test/regress/regress1/bv/bv-proof00.smt similarity index 100% rename from test/regress/regress0/bv/bv-proof00.smt rename to test/regress/regress1/bv/bv-proof00.smt diff --git a/test/regress/regress0/bv/fuzz34.smt b/test/regress/regress1/bv/fuzz34.smt similarity index 100% rename from test/regress/regress0/bv/fuzz34.smt rename to test/regress/regress1/bv/fuzz34.smt diff --git a/test/regress/regress0/bv/fuzz38.smt b/test/regress/regress1/bv/fuzz38.smt similarity index 100% rename from test/regress/regress0/bv/fuzz38.smt rename to test/regress/regress1/bv/fuzz38.smt diff --git a/test/regress/regress0/datatypes/manos-model.smt2 b/test/regress/regress1/datatypes/manos-model.smt2 similarity index 100% rename from test/regress/regress0/datatypes/manos-model.smt2 rename to test/regress/regress1/datatypes/manos-model.smt2 diff --git a/test/regress/regress0/decision/error3.smt b/test/regress/regress1/decision/error3.smt similarity index 100% rename from test/regress/regress0/decision/error3.smt rename to test/regress/regress1/decision/error3.smt diff --git a/test/regress/regress0/fmf/ForElimination-scala-9.smt2 b/test/regress/regress1/fmf/ForElimination-scala-9.smt2 similarity index 100% rename from test/regress/regress0/fmf/ForElimination-scala-9.smt2 rename to test/regress/regress1/fmf/ForElimination-scala-9.smt2 diff --git a/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt b/test/regress/regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt similarity index 100% rename from test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt rename to test/regress/regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt diff --git a/test/regress/regress0/lemmas/pursuit-safety-8.smt b/test/regress/regress1/lemmas/pursuit-safety-8.smt similarity index 100% rename from test/regress/regress0/lemmas/pursuit-safety-8.smt rename to test/regress/regress1/lemmas/pursuit-safety-8.smt diff --git a/test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt similarity index 100% rename from test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt rename to test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt diff --git a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 similarity index 100% rename from test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 rename to test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2 similarity index 100% rename from test/regress/regress0/rewriterules/read5.smt2 rename to test/regress/regress1/rewriterules/read5.smt2 diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2 similarity index 100% rename from test/regress/regress0/sep/loop-1220.smt2 rename to test/regress/regress1/sep/loop-1220.smt2 diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress1/sep/sep-simp-unc.smt2 similarity index 100% rename from test/regress/regress0/sep/sep-simp-unc.smt2 rename to test/regress/regress1/sep/sep-simp-unc.smt2 diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 similarity index 100% rename from test/regress/regress0/sep/split-find-unsat-w-emp.smt2 rename to test/regress/regress1/sep/split-find-unsat-w-emp.smt2 diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress1/sep/split-find-unsat.smt2 similarity index 100% rename from test/regress/regress0/sep/split-find-unsat.smt2 rename to test/regress/regress1/sep/split-find-unsat.smt2 diff --git a/test/regress/regress0/sets/card-vc6-minimized.smt2 b/test/regress/regress1/sets/card-vc6-minimized.smt2 similarity index 100% rename from test/regress/regress0/sets/card-vc6-minimized.smt2 rename to test/regress/regress1/sets/card-vc6-minimized.smt2 diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress1/sets/sets-disequal.smt2 similarity index 100% rename from test/regress/regress0/sets/sets-disequal.smt2 rename to test/regress/regress1/sets/sets-disequal.smt2 diff --git a/test/regress/regress0/strings/cmu-5042-0707-2.smt2 b/test/regress/regress1/strings/cmu-5042-0707-2.smt2 similarity index 100% rename from test/regress/regress0/strings/cmu-5042-0707-2.smt2 rename to test/regress/regress1/strings/cmu-5042-0707-2.smt2 diff --git a/test/regress/regress0/strings/cmu-dis-0707-3.smt2 b/test/regress/regress1/strings/cmu-dis-0707-3.smt2 similarity index 100% rename from test/regress/regress0/strings/cmu-dis-0707-3.smt2 rename to test/regress/regress1/strings/cmu-dis-0707-3.smt2 diff --git a/test/regress/regress0/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy similarity index 100% rename from test/regress/regress0/sygus/hd-sdiv.sy rename to test/regress/regress1/sygus/hd-sdiv.sy diff --git a/test/regress/regress1/DTP_k2_n35_c175_s15.smt2 b/test/regress/regress2/DTP_k2_n35_c175_s15.smt2 similarity index 100% rename from test/regress/regress1/DTP_k2_n35_c175_s15.smt2 rename to test/regress/regress2/DTP_k2_n35_c175_s15.smt2 diff --git a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 similarity index 100% rename from test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 rename to test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 diff --git a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect similarity index 100% rename from test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect rename to test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect diff --git a/test/regress/regress1/GEO123+1.minimized.smt2 b/test/regress/regress2/GEO123+1.minimized.smt2 similarity index 100% rename from test/regress/regress1/GEO123+1.minimized.smt2 rename to test/regress/regress2/GEO123+1.minimized.smt2 diff --git a/test/regress/regress2/Makefile b/test/regress/regress2/Makefile index 5a9aa63be..b720980f1 100644 --- a/test/regress/regress2/Makefile +++ b/test/regress/regress2/Makefile @@ -1,5 +1,5 @@ topdir = ../../.. -srcdir = test/regress/regress2 +srcdir = test/regress/regress1 include $(topdir)/Makefile.subdir diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 9deb1f37b..c47d5840c 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . +SUBDIRS = . arith # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) @@ -20,21 +20,35 @@ MAKEFLAGS = -k # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" -TESTS = bmc-ibm-1.smt \ - bmc-ibm-2.smt \ - bmc-ibm-5.smt \ - bmc-ibm-7.smt \ - friedman_n6_i4.smt \ - hole9.cvc \ - qwh.35.405.shuffled-as.sat03-1651.smt \ - eq_diamond14.smt \ - incorrect1.smt \ - incorrect2.smt \ - bug497.cvc \ - pp-regfile.smt +TESTS = bug136.smt \ + bug148.smt \ + bug394.smt2 \ + DTP_k2_n35_c175_s15.smt2 \ + GEO123+1.minimized.smt2 \ + error1.smt \ + friedman_n4_i5.smt \ + hole7.cvc \ + hole8.cvc \ + instance_1444.smt \ + fuzz_2.smt \ + hash_sat_10_09.smt2 \ + hash_sat_07_17.smt2 \ + ooo.tag10.smt2 \ + hash_sat_06_19.smt2 \ + hash_sat_09_09.smt2 \ + ooo.rf6.smt2 \ + auflia-fuzz06.smt \ + piVC_5581bd.smt2 \ + typed_v1l50016-simp.cvc \ + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ + xs-09-16-3-4-1-5.smt \ + xs-09-16-3-4-1-5.decn.smt \ + uflia-error0.smt2 EXTRA_DIST = $(TESTS) \ - pp-regfile.smt.expect + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ + uflia-error0.smt2.expect \ + xs-09-16-3-4-1-5.decn.smt.expect #if CVC4_BUILD_PROFILE_COMPETITION #else @@ -51,5 +65,5 @@ EXTRA_DIST = $(TESTS) \ regress regress2 test: check # do nothing in this subdir -.PHONY: regress0 regress1 regress3 -regress0 regress1 regress3: +.PHONY: regress0 regress1 regress3 regress4 +regress0 regress1 regress3 regress4: diff --git a/test/regress/regress1/arith/Makefile b/test/regress/regress2/arith/Makefile similarity index 100% rename from test/regress/regress1/arith/Makefile rename to test/regress/regress2/arith/Makefile diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress2/arith/Makefile.am similarity index 100% rename from test/regress/regress1/arith/Makefile.am rename to test/regress/regress2/arith/Makefile.am diff --git a/test/regress/regress1/arith/abz5_1400.smt b/test/regress/regress2/arith/abz5_1400.smt similarity index 100% rename from test/regress/regress1/arith/abz5_1400.smt rename to test/regress/regress2/arith/abz5_1400.smt diff --git a/test/regress/regress1/arith/lpsat-goal-9.smt2 b/test/regress/regress2/arith/lpsat-goal-9.smt2 similarity index 100% rename from test/regress/regress1/arith/lpsat-goal-9.smt2 rename to test/regress/regress2/arith/lpsat-goal-9.smt2 diff --git a/test/regress/regress1/arith/prp-13-24.smt2 b/test/regress/regress2/arith/prp-13-24.smt2 similarity index 100% rename from test/regress/regress1/arith/prp-13-24.smt2 rename to test/regress/regress2/arith/prp-13-24.smt2 diff --git a/test/regress/regress1/arith/pursuit-safety-11.smt b/test/regress/regress2/arith/pursuit-safety-11.smt similarity index 100% rename from test/regress/regress1/arith/pursuit-safety-11.smt rename to test/regress/regress2/arith/pursuit-safety-11.smt diff --git a/test/regress/regress1/arith/pursuit-safety-12.smt b/test/regress/regress2/arith/pursuit-safety-12.smt similarity index 100% rename from test/regress/regress1/arith/pursuit-safety-12.smt rename to test/regress/regress2/arith/pursuit-safety-12.smt diff --git a/test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2 b/test/regress/regress2/arith/qlock-4-10-9.base.cvc.smt2 similarity index 100% rename from test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2 rename to test/regress/regress2/arith/qlock-4-10-9.base.cvc.smt2 diff --git a/test/regress/regress1/arith/sc-7.base.cvc.smt b/test/regress/regress2/arith/sc-7.base.cvc.smt similarity index 100% rename from test/regress/regress1/arith/sc-7.base.cvc.smt rename to test/regress/regress2/arith/sc-7.base.cvc.smt diff --git a/test/regress/regress1/arith/uart-8.base.cvc.smt b/test/regress/regress2/arith/uart-8.base.cvc.smt similarity index 100% rename from test/regress/regress1/arith/uart-8.base.cvc.smt rename to test/regress/regress2/arith/uart-8.base.cvc.smt diff --git a/test/regress/regress1/auflia-fuzz06.smt b/test/regress/regress2/auflia-fuzz06.smt similarity index 100% rename from test/regress/regress1/auflia-fuzz06.smt rename to test/regress/regress2/auflia-fuzz06.smt diff --git a/test/regress/regress1/bug136.smt b/test/regress/regress2/bug136.smt similarity index 100% rename from test/regress/regress1/bug136.smt rename to test/regress/regress2/bug136.smt diff --git a/test/regress/regress1/bug148.smt b/test/regress/regress2/bug148.smt similarity index 100% rename from test/regress/regress1/bug148.smt rename to test/regress/regress2/bug148.smt diff --git a/test/regress/regress1/bug394.smt2 b/test/regress/regress2/bug394.smt2 similarity index 100% rename from test/regress/regress1/bug394.smt2 rename to test/regress/regress2/bug394.smt2 diff --git a/test/regress/regress1/error0.smt2 b/test/regress/regress2/error0.smt2 similarity index 100% rename from test/regress/regress1/error0.smt2 rename to test/regress/regress2/error0.smt2 diff --git a/test/regress/regress1/error1.smt b/test/regress/regress2/error1.smt similarity index 100% rename from test/regress/regress1/error1.smt rename to test/regress/regress2/error1.smt diff --git a/test/regress/regress1/friedman_n4_i5.smt b/test/regress/regress2/friedman_n4_i5.smt similarity index 100% rename from test/regress/regress1/friedman_n4_i5.smt rename to test/regress/regress2/friedman_n4_i5.smt diff --git a/test/regress/regress1/fuzz_2.smt b/test/regress/regress2/fuzz_2.smt similarity index 100% rename from test/regress/regress1/fuzz_2.smt rename to test/regress/regress2/fuzz_2.smt diff --git a/test/regress/regress1/hash_sat_06_19.smt2 b/test/regress/regress2/hash_sat_06_19.smt2 similarity index 100% rename from test/regress/regress1/hash_sat_06_19.smt2 rename to test/regress/regress2/hash_sat_06_19.smt2 diff --git a/test/regress/regress1/hash_sat_07_17.smt2 b/test/regress/regress2/hash_sat_07_17.smt2 similarity index 100% rename from test/regress/regress1/hash_sat_07_17.smt2 rename to test/regress/regress2/hash_sat_07_17.smt2 diff --git a/test/regress/regress1/hash_sat_09_09.smt2 b/test/regress/regress2/hash_sat_09_09.smt2 similarity index 100% rename from test/regress/regress1/hash_sat_09_09.smt2 rename to test/regress/regress2/hash_sat_09_09.smt2 diff --git a/test/regress/regress1/hash_sat_10_09.smt2 b/test/regress/regress2/hash_sat_10_09.smt2 similarity index 100% rename from test/regress/regress1/hash_sat_10_09.smt2 rename to test/regress/regress2/hash_sat_10_09.smt2 diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress2/hole7.cvc similarity index 100% rename from test/regress/regress1/hole7.cvc rename to test/regress/regress2/hole7.cvc diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress2/hole8.cvc similarity index 100% rename from test/regress/regress1/hole8.cvc rename to test/regress/regress2/hole8.cvc diff --git a/test/regress/regress1/instance_1444.smt b/test/regress/regress2/instance_1444.smt similarity index 100% rename from test/regress/regress1/instance_1444.smt rename to test/regress/regress2/instance_1444.smt diff --git a/test/regress/regress1/ooo.rf6.smt2 b/test/regress/regress2/ooo.rf6.smt2 similarity index 100% rename from test/regress/regress1/ooo.rf6.smt2 rename to test/regress/regress2/ooo.rf6.smt2 diff --git a/test/regress/regress1/ooo.tag10.smt2 b/test/regress/regress2/ooo.tag10.smt2 similarity index 100% rename from test/regress/regress1/ooo.tag10.smt2 rename to test/regress/regress2/ooo.tag10.smt2 diff --git a/test/regress/regress1/piVC_5581bd.smt2 b/test/regress/regress2/piVC_5581bd.smt2 similarity index 100% rename from test/regress/regress1/piVC_5581bd.smt2 rename to test/regress/regress2/piVC_5581bd.smt2 diff --git a/test/regress/regress1/typed_v1l50016-simp.cvc b/test/regress/regress2/typed_v1l50016-simp.cvc similarity index 100% rename from test/regress/regress1/typed_v1l50016-simp.cvc rename to test/regress/regress2/typed_v1l50016-simp.cvc diff --git a/test/regress/regress1/uflia-error0.smt2 b/test/regress/regress2/uflia-error0.smt2 similarity index 100% rename from test/regress/regress1/uflia-error0.smt2 rename to test/regress/regress2/uflia-error0.smt2 diff --git a/test/regress/regress1/uflia-error0.smt2.expect b/test/regress/regress2/uflia-error0.smt2.expect similarity index 100% rename from test/regress/regress1/uflia-error0.smt2.expect rename to test/regress/regress2/uflia-error0.smt2.expect diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt similarity index 100% rename from test/regress/regress1/xs-09-16-3-4-1-5.decn.smt rename to test/regress/regress2/xs-09-16-3-4-1-5.decn.smt diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect similarity index 100% rename from test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect rename to test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.smt b/test/regress/regress2/xs-09-16-3-4-1-5.smt similarity index 100% rename from test/regress/regress1/xs-09-16-3-4-1-5.smt rename to test/regress/regress2/xs-09-16-3-4-1-5.smt diff --git a/test/regress/regress1/xs-11-20-5-2-5-3.smt b/test/regress/regress2/xs-11-20-5-2-5-3.smt similarity index 100% rename from test/regress/regress1/xs-11-20-5-2-5-3.smt rename to test/regress/regress2/xs-11-20-5-2-5-3.smt diff --git a/test/regress/regress1/xs-11-20-5-2-5-3.smt2 b/test/regress/regress2/xs-11-20-5-2-5-3.smt2 similarity index 100% rename from test/regress/regress1/xs-11-20-5-2-5-3.smt2 rename to test/regress/regress2/xs-11-20-5-2-5-3.smt2 diff --git a/test/regress/regress3/Makefile b/test/regress/regress3/Makefile index 223547305..5a9aa63be 100644 --- a/test/regress/regress3/Makefile +++ b/test/regress/regress3/Makefile @@ -1,5 +1,5 @@ topdir = ../../.. -srcdir = test/regress/regress3 +srcdir = test/regress/regress2 include $(topdir)/Makefile.subdir diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 3fb798bcc..f45c5bd64 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -20,14 +20,21 @@ MAKEFLAGS = -k # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" -TESTS = bug143.smt \ - C880mul.miter.shuffled-as.sat03-348.smt \ - comb2.shuffled-as.sat03-420.smt \ - hole10.cvc \ - instance_1151.smt \ - NEQ016_size5.smt - -EXTRA_DIST = $(TESTS) +TESTS = bmc-ibm-1.smt \ + bmc-ibm-2.smt \ + bmc-ibm-5.smt \ + bmc-ibm-7.smt \ + friedman_n6_i4.smt \ + hole9.cvc \ + qwh.35.405.shuffled-as.sat03-1651.smt \ + eq_diamond14.smt \ + incorrect1.smt \ + incorrect2.smt \ + bug497.cvc \ + pp-regfile.smt + +EXTRA_DIST = $(TESTS) \ + pp-regfile.smt.expect #if CVC4_BUILD_PROFILE_COMPETITION #else @@ -44,5 +51,5 @@ EXTRA_DIST = $(TESTS) regress regress3 test: check # do nothing in this subdir -.PHONY: regress0 regress1 regress2 -regress0 regress1 regress2: +.PHONY: regress0 regress1 regress2 regress4 +regress0 regress1 regress2 regress4: diff --git a/test/regress/regress2/bmc-ibm-1.smt b/test/regress/regress3/bmc-ibm-1.smt similarity index 100% rename from test/regress/regress2/bmc-ibm-1.smt rename to test/regress/regress3/bmc-ibm-1.smt diff --git a/test/regress/regress2/bmc-ibm-2.smt b/test/regress/regress3/bmc-ibm-2.smt similarity index 100% rename from test/regress/regress2/bmc-ibm-2.smt rename to test/regress/regress3/bmc-ibm-2.smt diff --git a/test/regress/regress2/bmc-ibm-5.smt b/test/regress/regress3/bmc-ibm-5.smt similarity index 100% rename from test/regress/regress2/bmc-ibm-5.smt rename to test/regress/regress3/bmc-ibm-5.smt diff --git a/test/regress/regress2/bmc-ibm-7.smt b/test/regress/regress3/bmc-ibm-7.smt similarity index 100% rename from test/regress/regress2/bmc-ibm-7.smt rename to test/regress/regress3/bmc-ibm-7.smt diff --git a/test/regress/regress2/bug497.cvc b/test/regress/regress3/bug497.cvc similarity index 100% rename from test/regress/regress2/bug497.cvc rename to test/regress/regress3/bug497.cvc diff --git a/test/regress/regress2/eq_diamond14.smt b/test/regress/regress3/eq_diamond14.smt similarity index 100% rename from test/regress/regress2/eq_diamond14.smt rename to test/regress/regress3/eq_diamond14.smt diff --git a/test/regress/regress2/friedman_n6_i4.smt b/test/regress/regress3/friedman_n6_i4.smt similarity index 100% rename from test/regress/regress2/friedman_n6_i4.smt rename to test/regress/regress3/friedman_n6_i4.smt diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress3/hole9.cvc similarity index 100% rename from test/regress/regress2/hole9.cvc rename to test/regress/regress3/hole9.cvc diff --git a/test/regress/regress2/incorrect1.smt b/test/regress/regress3/incorrect1.smt similarity index 100% rename from test/regress/regress2/incorrect1.smt rename to test/regress/regress3/incorrect1.smt diff --git a/test/regress/regress2/incorrect2.smt b/test/regress/regress3/incorrect2.smt similarity index 100% rename from test/regress/regress2/incorrect2.smt rename to test/regress/regress3/incorrect2.smt diff --git a/test/regress/regress2/pp-regfile.smt b/test/regress/regress3/pp-regfile.smt similarity index 100% rename from test/regress/regress2/pp-regfile.smt rename to test/regress/regress3/pp-regfile.smt diff --git a/test/regress/regress2/pp-regfile.smt.expect b/test/regress/regress3/pp-regfile.smt.expect similarity index 100% rename from test/regress/regress2/pp-regfile.smt.expect rename to test/regress/regress3/pp-regfile.smt.expect diff --git a/test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt b/test/regress/regress3/qwh.35.405.shuffled-as.sat03-1651.smt similarity index 100% rename from test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt rename to test/regress/regress3/qwh.35.405.shuffled-as.sat03-1651.smt diff --git a/test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt b/test/regress/regress4/C880mul.miter.shuffled-as.sat03-348.smt similarity index 100% rename from test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt rename to test/regress/regress4/C880mul.miter.shuffled-as.sat03-348.smt diff --git a/test/regress/regress1/Makefile b/test/regress/regress4/Makefile similarity index 76% rename from test/regress/regress1/Makefile rename to test/regress/regress4/Makefile index b720980f1..223547305 100644 --- a/test/regress/regress1/Makefile +++ b/test/regress/regress4/Makefile @@ -1,5 +1,5 @@ topdir = ../../.. -srcdir = test/regress/regress1 +srcdir = test/regress/regress3 include $(topdir)/Makefile.subdir diff --git a/test/regress/regress4/Makefile.am b/test/regress/regress4/Makefile.am new file mode 100644 index 000000000..5a31fb24e --- /dev/null +++ b/test/regress/regress4/Makefile.am @@ -0,0 +1,48 @@ +SUBDIRS = . + +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = bug143.smt \ + C880mul.miter.shuffled-as.sat03-348.smt \ + comb2.shuffled-as.sat03-420.smt \ + hole10.cvc \ + instance_1151.smt \ + NEQ016_size5.smt + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" in this directory +.PHONY: regress regress4 test +regress regress4 test: check + +# do nothing in this subdir +.PHONY: regress0 regress1 regress2 regress3 +regress0 regress1 regress2 regress3: diff --git a/test/regress/regress3/NEQ016_size5.smt b/test/regress/regress4/NEQ016_size5.smt similarity index 100% rename from test/regress/regress3/NEQ016_size5.smt rename to test/regress/regress4/NEQ016_size5.smt diff --git a/test/regress/regress3/bug143.smt b/test/regress/regress4/bug143.smt similarity index 100% rename from test/regress/regress3/bug143.smt rename to test/regress/regress4/bug143.smt diff --git a/test/regress/regress3/comb2.shuffled-as.sat03-420.smt b/test/regress/regress4/comb2.shuffled-as.sat03-420.smt similarity index 100% rename from test/regress/regress3/comb2.shuffled-as.sat03-420.smt rename to test/regress/regress4/comb2.shuffled-as.sat03-420.smt diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress4/hole10.cvc similarity index 100% rename from test/regress/regress3/hole10.cvc rename to test/regress/regress4/hole10.cvc diff --git a/test/regress/regress3/instance_1151.smt b/test/regress/regress4/instance_1151.smt similarity index 100% rename from test/regress/regress3/instance_1151.smt rename to test/regress/regress4/instance_1151.smt -- 2.30.2