diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/auflia/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/bv/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/decision/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/lemmas/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/rewriterules/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/sep/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress1/Makefile.am | 50 | ||||
-rw-r--r-- | test/regress/regress1/aufbv/fuzz10.smt (renamed from test/regress/regress0/aufbv/fuzz10.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/auflia/bug330.smt2 (renamed from test/regress/regress0/auflia/bug330.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bug425.cvc (renamed from test/regress/regress0/bug425.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bug519.smt2 (renamed from test/regress/regress0/bug519.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bug521.smt2 (renamed from test/regress/regress0/bug521.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bv/bv-proof00.smt (renamed from test/regress/regress0/bv/bv-proof00.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bv/fuzz34.smt (renamed from test/regress/regress0/bv/fuzz34.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/bv/fuzz38.smt (renamed from test/regress/regress0/bv/fuzz38.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/datatypes/manos-model.smt2 (renamed from test/regress/regress0/datatypes/manos-model.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/decision/error3.smt (renamed from test/regress/regress0/decision/error3.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/fmf/ForElimination-scala-9.smt2 (renamed from test/regress/regress0/fmf/ForElimination-scala-9.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt (renamed from test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/lemmas/pursuit-safety-8.smt (renamed from test/regress/regress0/lemmas/pursuit-safety-8.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt (renamed from test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 (renamed from test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/rewriterules/read5.smt2 (renamed from test/regress/regress0/rewriterules/read5.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/sep/loop-1220.smt2 (renamed from test/regress/regress0/sep/loop-1220.smt2) | 0 | ||||
-rwxr-xr-x | test/regress/regress1/sep/sep-simp-unc.smt2 (renamed from test/regress/regress0/sep/sep-simp-unc.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/sep/split-find-unsat-w-emp.smt2 (renamed from test/regress/regress0/sep/split-find-unsat-w-emp.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/sep/split-find-unsat.smt2 (renamed from test/regress/regress0/sep/split-find-unsat.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/sets/card-vc6-minimized.smt2 (renamed from test/regress/regress0/sets/card-vc6-minimized.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/sets/sets-disequal.smt2 (renamed from test/regress/regress0/sets/sets-disequal.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/strings/cmu-5042-0707-2.smt2 (renamed from test/regress/regress0/strings/cmu-5042-0707-2.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/strings/cmu-dis-0707-3.smt2 (renamed from test/regress/regress0/strings/cmu-dis-0707-3.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/sygus/hd-sdiv.sy (renamed from test/regress/regress0/sygus/hd-sdiv.sy) | 0 | ||||
-rw-r--r-- | test/regress/regress2/DTP_k2_n35_c175_s15.smt2 (renamed from test/regress/regress1/DTP_k2_n35_c175_s15.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 (renamed from test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect (renamed from test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect) | 0 | ||||
-rw-r--r-- | test/regress/regress2/GEO123+1.minimized.smt2 (renamed from test/regress/regress1/GEO123+1.minimized.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/Makefile | 2 | ||||
-rw-r--r-- | test/regress/regress2/Makefile.am | 46 | ||||
-rw-r--r-- | test/regress/regress2/arith/Makefile (renamed from test/regress/regress1/arith/Makefile) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/Makefile.am (renamed from test/regress/regress1/arith/Makefile.am) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/abz5_1400.smt (renamed from test/regress/regress1/arith/abz5_1400.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/lpsat-goal-9.smt2 (renamed from test/regress/regress1/arith/lpsat-goal-9.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/prp-13-24.smt2 (renamed from test/regress/regress1/arith/prp-13-24.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/pursuit-safety-11.smt (renamed from test/regress/regress1/arith/pursuit-safety-11.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/pursuit-safety-12.smt (renamed from test/regress/regress1/arith/pursuit-safety-12.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/qlock-4-10-9.base.cvc.smt2 (renamed from test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/sc-7.base.cvc.smt (renamed from test/regress/regress1/arith/sc-7.base.cvc.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/arith/uart-8.base.cvc.smt (renamed from test/regress/regress1/arith/uart-8.base.cvc.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/auflia-fuzz06.smt (renamed from test/regress/regress1/auflia-fuzz06.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bug136.smt (renamed from test/regress/regress1/bug136.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bug148.smt (renamed from test/regress/regress1/bug148.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bug394.smt2 (renamed from test/regress/regress1/bug394.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/error0.smt2 (renamed from test/regress/regress1/error0.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/error1.smt (renamed from test/regress/regress1/error1.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/friedman_n4_i5.smt (renamed from test/regress/regress1/friedman_n4_i5.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/fuzz_2.smt (renamed from test/regress/regress1/fuzz_2.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/hash_sat_06_19.smt2 (renamed from test/regress/regress1/hash_sat_06_19.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/hash_sat_07_17.smt2 (renamed from test/regress/regress1/hash_sat_07_17.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/hash_sat_09_09.smt2 (renamed from test/regress/regress1/hash_sat_09_09.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/hash_sat_10_09.smt2 (renamed from test/regress/regress1/hash_sat_10_09.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/hole7.cvc (renamed from test/regress/regress1/hole7.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress2/hole8.cvc (renamed from test/regress/regress1/hole8.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress2/instance_1444.smt (renamed from test/regress/regress1/instance_1444.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/ooo.rf6.smt2 (renamed from test/regress/regress1/ooo.rf6.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/ooo.tag10.smt2 (renamed from test/regress/regress1/ooo.tag10.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/piVC_5581bd.smt2 (renamed from test/regress/regress1/piVC_5581bd.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/typed_v1l50016-simp.cvc (renamed from test/regress/regress1/typed_v1l50016-simp.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress2/uflia-error0.smt2 (renamed from test/regress/regress1/uflia-error0.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress2/uflia-error0.smt2.expect (renamed from test/regress/regress1/uflia-error0.smt2.expect) | 0 | ||||
-rw-r--r-- | test/regress/regress2/xs-09-16-3-4-1-5.decn.smt (renamed from test/regress/regress1/xs-09-16-3-4-1-5.decn.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect (renamed from test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect) | 0 | ||||
-rw-r--r-- | test/regress/regress2/xs-09-16-3-4-1-5.smt (renamed from test/regress/regress1/xs-09-16-3-4-1-5.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/xs-11-20-5-2-5-3.smt (renamed from test/regress/regress1/xs-11-20-5-2-5-3.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/xs-11-20-5-2-5-3.smt2 (renamed from test/regress/regress1/xs-11-20-5-2-5-3.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress3/Makefile | 2 | ||||
-rw-r--r-- | test/regress/regress3/Makefile.am | 27 | ||||
-rw-r--r-- | test/regress/regress3/bmc-ibm-1.smt (renamed from test/regress/regress2/bmc-ibm-1.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/bmc-ibm-2.smt (renamed from test/regress/regress2/bmc-ibm-2.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/bmc-ibm-5.smt (renamed from test/regress/regress2/bmc-ibm-5.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/bmc-ibm-7.smt (renamed from test/regress/regress2/bmc-ibm-7.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/bug497.cvc (renamed from test/regress/regress2/bug497.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress3/eq_diamond14.smt (renamed from test/regress/regress2/eq_diamond14.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/friedman_n6_i4.smt (renamed from test/regress/regress2/friedman_n6_i4.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/hole9.cvc (renamed from test/regress/regress2/hole9.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress3/incorrect1.smt (renamed from test/regress/regress2/incorrect1.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/incorrect2.smt (renamed from test/regress/regress2/incorrect2.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/pp-regfile.smt (renamed from test/regress/regress2/pp-regfile.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/pp-regfile.smt.expect (renamed from test/regress/regress2/pp-regfile.smt.expect) | 0 | ||||
-rw-r--r-- | test/regress/regress3/qwh.35.405.shuffled-as.sat03-1651.smt (renamed from test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress4/C880mul.miter.shuffled-as.sat03-348.smt (renamed from test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress4/Makefile (renamed from test/regress/regress1/Makefile) | 2 | ||||
-rw-r--r-- | test/regress/regress4/Makefile.am | 48 | ||||
-rw-r--r-- | test/regress/regress4/NEQ016_size5.smt (renamed from test/regress/regress3/NEQ016_size5.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress4/bug143.smt (renamed from test/regress/regress3/bug143.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress4/comb2.shuffled-as.sat03-420.smt (renamed from test/regress/regress3/comb2.shuffled-as.sat03-420.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress4/hole10.cvc (renamed from test/regress/regress3/hole10.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress4/instance_1151.smt (renamed from test/regress/regress3/instance_1151.smt) | 0 |
104 files changed, 111 insertions, 101 deletions
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 index b838f80f0..b838f80f0 100644 --- a/test/regress/regress0/aufbv/fuzz10.smt +++ b/test/regress/regress1/aufbv/fuzz10.smt diff --git a/test/regress/regress0/auflia/bug330.smt2 b/test/regress/regress1/auflia/bug330.smt2 index d05a8b2a0..d05a8b2a0 100644 --- a/test/regress/regress0/auflia/bug330.smt2 +++ b/test/regress/regress1/auflia/bug330.smt2 diff --git a/test/regress/regress0/bug425.cvc b/test/regress/regress1/bug425.cvc index 5b6464c32..5b6464c32 100644 --- a/test/regress/regress0/bug425.cvc +++ b/test/regress/regress1/bug425.cvc diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress1/bug519.smt2 index 72ec634a8..72ec634a8 100644 --- a/test/regress/regress0/bug519.smt2 +++ b/test/regress/regress1/bug519.smt2 diff --git a/test/regress/regress0/bug521.smt2 b/test/regress/regress1/bug521.smt2 index 8f840a1f6..8f840a1f6 100644 --- a/test/regress/regress0/bug521.smt2 +++ b/test/regress/regress1/bug521.smt2 diff --git a/test/regress/regress0/bv/bv-proof00.smt b/test/regress/regress1/bv/bv-proof00.smt index adfebf58e..adfebf58e 100644 --- a/test/regress/regress0/bv/bv-proof00.smt +++ b/test/regress/regress1/bv/bv-proof00.smt diff --git a/test/regress/regress0/bv/fuzz34.smt b/test/regress/regress1/bv/fuzz34.smt index 200bed99f..200bed99f 100644 --- a/test/regress/regress0/bv/fuzz34.smt +++ b/test/regress/regress1/bv/fuzz34.smt diff --git a/test/regress/regress0/bv/fuzz38.smt b/test/regress/regress1/bv/fuzz38.smt index 39ebe9e42..39ebe9e42 100644 --- a/test/regress/regress0/bv/fuzz38.smt +++ b/test/regress/regress1/bv/fuzz38.smt diff --git a/test/regress/regress0/datatypes/manos-model.smt2 b/test/regress/regress1/datatypes/manos-model.smt2 index 4ade71151..4ade71151 100644 --- a/test/regress/regress0/datatypes/manos-model.smt2 +++ b/test/regress/regress1/datatypes/manos-model.smt2 diff --git a/test/regress/regress0/decision/error3.smt b/test/regress/regress1/decision/error3.smt index 36c409f3f..36c409f3f 100644 --- a/test/regress/regress0/decision/error3.smt +++ b/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 index 36bb915f4..36bb915f4 100644 --- a/test/regress/regress0/fmf/ForElimination-scala-9.smt2 +++ b/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 index 92cc1b080..92cc1b080 100644 --- a/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt +++ b/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 index 5985c500b..5985c500b 100644 --- a/test/regress/regress0/lemmas/pursuit-safety-8.smt +++ b/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 index 506b99b46..506b99b46 100644 --- a/test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt +++ b/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 index 13f7234e9..13f7234e9 100644 --- a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 +++ b/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 index e66df7c7e..e66df7c7e 100644 --- a/test/regress/regress0/rewriterules/read5.smt2 +++ b/test/regress/regress1/rewriterules/read5.smt2 diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2 index b857aec2a..b857aec2a 100644 --- a/test/regress/regress0/sep/loop-1220.smt2 +++ b/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 index cedbb53eb..cedbb53eb 100755 --- a/test/regress/regress0/sep/sep-simp-unc.smt2 +++ b/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 index 10e509e05..10e509e05 100644 --- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 +++ b/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 index 1a9e76a8a..1a9e76a8a 100644 --- a/test/regress/regress0/sep/split-find-unsat.smt2 +++ b/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 index d7f4bdf1e..d7f4bdf1e 100644 --- a/test/regress/regress0/sets/card-vc6-minimized.smt2 +++ b/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 index 3acf77108..3acf77108 100644 --- a/test/regress/regress0/sets/sets-disequal.smt2 +++ b/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 index 637142dfb..637142dfb 100644 --- a/test/regress/regress0/strings/cmu-5042-0707-2.smt2 +++ b/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 index 209cbb3f9..209cbb3f9 100644 --- a/test/regress/regress0/strings/cmu-dis-0707-3.smt2 +++ b/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 index 019b48a1c..019b48a1c 100644 --- a/test/regress/regress0/sygus/hd-sdiv.sy +++ b/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 index 20f4bf5a9..20f4bf5a9 100644 --- a/test/regress/regress1/DTP_k2_n35_c175_s15.smt2 +++ b/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 index 25f006d30..25f006d30 100644 --- 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 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 index 7cb6ba8c2..7cb6ba8c2 100644 --- 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 diff --git a/test/regress/regress1/GEO123+1.minimized.smt2 b/test/regress/regress2/GEO123+1.minimized.smt2 index 764c41699..764c41699 100644 --- a/test/regress/regress1/GEO123+1.minimized.smt2 +++ b/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 index 481d240e4..481d240e4 100644 --- a/test/regress/regress1/arith/Makefile +++ b/test/regress/regress2/arith/Makefile diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress2/arith/Makefile.am index fff5372c6..fff5372c6 100644 --- a/test/regress/regress1/arith/Makefile.am +++ b/test/regress/regress2/arith/Makefile.am diff --git a/test/regress/regress1/arith/abz5_1400.smt b/test/regress/regress2/arith/abz5_1400.smt index 662b39859..662b39859 100644 --- a/test/regress/regress1/arith/abz5_1400.smt +++ b/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 index d71fc1340..d71fc1340 100644 --- a/test/regress/regress1/arith/lpsat-goal-9.smt2 +++ b/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 index b3b8e69b1..b3b8e69b1 100644 --- a/test/regress/regress1/arith/prp-13-24.smt2 +++ b/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 index 1c12e0770..1c12e0770 100644 --- a/test/regress/regress1/arith/pursuit-safety-11.smt +++ b/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 index 8f79b3d92..8f79b3d92 100644 --- a/test/regress/regress1/arith/pursuit-safety-12.smt +++ b/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 index d71fc1340..d71fc1340 100644 --- a/test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2 +++ b/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 index 72a561593..72a561593 100644 --- a/test/regress/regress1/arith/sc-7.base.cvc.smt +++ b/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 index a64a0cdbe..a64a0cdbe 100644 --- a/test/regress/regress1/arith/uart-8.base.cvc.smt +++ b/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 index 88c2a9d5c..88c2a9d5c 100644 --- a/test/regress/regress1/auflia-fuzz06.smt +++ b/test/regress/regress2/auflia-fuzz06.smt diff --git a/test/regress/regress1/bug136.smt b/test/regress/regress2/bug136.smt index 08fb3cb6c..08fb3cb6c 100644 --- a/test/regress/regress1/bug136.smt +++ b/test/regress/regress2/bug136.smt diff --git a/test/regress/regress1/bug148.smt b/test/regress/regress2/bug148.smt index a07dc1bf0..a07dc1bf0 100644 --- a/test/regress/regress1/bug148.smt +++ b/test/regress/regress2/bug148.smt diff --git a/test/regress/regress1/bug394.smt2 b/test/regress/regress2/bug394.smt2 index 99e19e7fb..99e19e7fb 100644 --- a/test/regress/regress1/bug394.smt2 +++ b/test/regress/regress2/bug394.smt2 diff --git a/test/regress/regress1/error0.smt2 b/test/regress/regress2/error0.smt2 index 73177a252..73177a252 100644 --- a/test/regress/regress1/error0.smt2 +++ b/test/regress/regress2/error0.smt2 diff --git a/test/regress/regress1/error1.smt b/test/regress/regress2/error1.smt index 9b2cabedf..9b2cabedf 100644 --- a/test/regress/regress1/error1.smt +++ b/test/regress/regress2/error1.smt diff --git a/test/regress/regress1/friedman_n4_i5.smt b/test/regress/regress2/friedman_n4_i5.smt index ff5c75735..ff5c75735 100644 --- a/test/regress/regress1/friedman_n4_i5.smt +++ b/test/regress/regress2/friedman_n4_i5.smt diff --git a/test/regress/regress1/fuzz_2.smt b/test/regress/regress2/fuzz_2.smt index 1dc2f619d..1dc2f619d 100644 --- a/test/regress/regress1/fuzz_2.smt +++ b/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 index b565a4b57..b565a4b57 100644 --- a/test/regress/regress1/hash_sat_06_19.smt2 +++ b/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 index 0bb49801a..0bb49801a 100644 --- a/test/regress/regress1/hash_sat_07_17.smt2 +++ b/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 index 6dc26542e..6dc26542e 100644 --- a/test/regress/regress1/hash_sat_09_09.smt2 +++ b/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 index 20cff8b1b..20cff8b1b 100644 --- a/test/regress/regress1/hash_sat_10_09.smt2 +++ b/test/regress/regress2/hash_sat_10_09.smt2 diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress2/hole7.cvc index 1f762477a..1f762477a 100644 --- a/test/regress/regress1/hole7.cvc +++ b/test/regress/regress2/hole7.cvc diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress2/hole8.cvc index 705c95ea6..705c95ea6 100644 --- a/test/regress/regress1/hole8.cvc +++ b/test/regress/regress2/hole8.cvc diff --git a/test/regress/regress1/instance_1444.smt b/test/regress/regress2/instance_1444.smt index 1bed83467..1bed83467 100644 --- a/test/regress/regress1/instance_1444.smt +++ b/test/regress/regress2/instance_1444.smt diff --git a/test/regress/regress1/ooo.rf6.smt2 b/test/regress/regress2/ooo.rf6.smt2 index 4860a3428..4860a3428 100644 --- a/test/regress/regress1/ooo.rf6.smt2 +++ b/test/regress/regress2/ooo.rf6.smt2 diff --git a/test/regress/regress1/ooo.tag10.smt2 b/test/regress/regress2/ooo.tag10.smt2 index ef8e2244c..ef8e2244c 100644 --- a/test/regress/regress1/ooo.tag10.smt2 +++ b/test/regress/regress2/ooo.tag10.smt2 diff --git a/test/regress/regress1/piVC_5581bd.smt2 b/test/regress/regress2/piVC_5581bd.smt2 index 78baeea84..78baeea84 100644 --- a/test/regress/regress1/piVC_5581bd.smt2 +++ b/test/regress/regress2/piVC_5581bd.smt2 diff --git a/test/regress/regress1/typed_v1l50016-simp.cvc b/test/regress/regress2/typed_v1l50016-simp.cvc index b4a1e4b32..b4a1e4b32 100644 --- a/test/regress/regress1/typed_v1l50016-simp.cvc +++ b/test/regress/regress2/typed_v1l50016-simp.cvc diff --git a/test/regress/regress1/uflia-error0.smt2 b/test/regress/regress2/uflia-error0.smt2 index 73177a252..73177a252 100644 --- a/test/regress/regress1/uflia-error0.smt2 +++ b/test/regress/regress2/uflia-error0.smt2 diff --git a/test/regress/regress1/uflia-error0.smt2.expect b/test/regress/regress2/uflia-error0.smt2.expect index 7fd1d5a98..7fd1d5a98 100644 --- a/test/regress/regress1/uflia-error0.smt2.expect +++ b/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 index 549306c5b..549306c5b 100644 --- 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 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 index 7fd1d5a98..7fd1d5a98 100644 --- 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 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 index 549306c5b..549306c5b 100644 --- a/test/regress/regress1/xs-09-16-3-4-1-5.smt +++ b/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 index 00ca325e1..00ca325e1 100644 --- a/test/regress/regress1/xs-11-20-5-2-5-3.smt +++ b/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 index bdf0d25ab..bdf0d25ab 100644 --- a/test/regress/regress1/xs-11-20-5-2-5-3.smt2 +++ b/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 index 9c210e3a1..9c210e3a1 100644 --- a/test/regress/regress2/bmc-ibm-1.smt +++ b/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 index 5f90bc620..5f90bc620 100644 --- a/test/regress/regress2/bmc-ibm-2.smt +++ b/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 index ba9020762..ba9020762 100644 --- a/test/regress/regress2/bmc-ibm-5.smt +++ b/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 index 3e8fd9321..3e8fd9321 100644 --- a/test/regress/regress2/bmc-ibm-7.smt +++ b/test/regress/regress3/bmc-ibm-7.smt diff --git a/test/regress/regress2/bug497.cvc b/test/regress/regress3/bug497.cvc index 8af568459..8af568459 100644 --- a/test/regress/regress2/bug497.cvc +++ b/test/regress/regress3/bug497.cvc diff --git a/test/regress/regress2/eq_diamond14.smt b/test/regress/regress3/eq_diamond14.smt index f89d0e3b7..f89d0e3b7 100644 --- a/test/regress/regress2/eq_diamond14.smt +++ b/test/regress/regress3/eq_diamond14.smt diff --git a/test/regress/regress2/friedman_n6_i4.smt b/test/regress/regress3/friedman_n6_i4.smt index 113877982..113877982 100644 --- a/test/regress/regress2/friedman_n6_i4.smt +++ b/test/regress/regress3/friedman_n6_i4.smt diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress3/hole9.cvc index e60839f7b..e60839f7b 100644 --- a/test/regress/regress2/hole9.cvc +++ b/test/regress/regress3/hole9.cvc diff --git a/test/regress/regress2/incorrect1.smt b/test/regress/regress3/incorrect1.smt index 23425d462..23425d462 100644 --- a/test/regress/regress2/incorrect1.smt +++ b/test/regress/regress3/incorrect1.smt diff --git a/test/regress/regress2/incorrect2.smt b/test/regress/regress3/incorrect2.smt index 23425d462..23425d462 100644 --- a/test/regress/regress2/incorrect2.smt +++ b/test/regress/regress3/incorrect2.smt diff --git a/test/regress/regress2/pp-regfile.smt b/test/regress/regress3/pp-regfile.smt index e60be055a..e60be055a 100644 --- a/test/regress/regress2/pp-regfile.smt +++ b/test/regress/regress3/pp-regfile.smt diff --git a/test/regress/regress2/pp-regfile.smt.expect b/test/regress/regress3/pp-regfile.smt.expect index 7fd1d5a98..7fd1d5a98 100644 --- a/test/regress/regress2/pp-regfile.smt.expect +++ b/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 index 7c09b58aa..7c09b58aa 100644 --- a/test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt +++ b/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 index 0cce52b17..0cce52b17 100644 --- a/test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt +++ b/test/regress/regress4/C880mul.miter.shuffled-as.sat03-348.smt diff --git a/test/regress/regress1/Makefile b/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 index ec56385f6..ec56385f6 100644 --- a/test/regress/regress3/NEQ016_size5.smt +++ b/test/regress/regress4/NEQ016_size5.smt diff --git a/test/regress/regress3/bug143.smt b/test/regress/regress4/bug143.smt index 21c588ad3..21c588ad3 100644 --- a/test/regress/regress3/bug143.smt +++ b/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 index b1d9309a3..b1d9309a3 100644 --- a/test/regress/regress3/comb2.shuffled-as.sat03-420.smt +++ b/test/regress/regress4/comb2.shuffled-as.sat03-420.smt diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress4/hole10.cvc index ebc8279d3..ebc8279d3 100644 --- a/test/regress/regress3/hole10.cvc +++ b/test/regress/regress4/hole10.cvc diff --git a/test/regress/regress3/instance_1151.smt b/test/regress/regress4/instance_1151.smt index 0d5bd0beb..0d5bd0beb 100644 --- a/test/regress/regress3/instance_1151.smt +++ b/test/regress/regress4/instance_1151.smt |