git.libre-soc.org Git - cvc5.git/commit

author	ajreynol <andrew.j.reynolds@gmail.com>
	Fri, 21 Oct 2016 19:01:17 +0000 (14:01 -0500)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Fri, 21 Oct 2016 19:01:17 +0000 (14:01 -0500)
commit	01d6e3933a3d733d3c1b5486ce1df8389cd6a176
tree	3110c0a54c0466862da0c7537b90013dab6a6479	tree
parent	3e93fdba8102e4ad1399af78967fec3d0495722a	commit \| diff

Move slow regress0 benchmarks to regress1, increment regress1 through regress3.

189 files changed:

test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/aufbv/Makefile.am		diff \| blob \| history
test/regress/regress0/aufbv/fuzz10.smt	[deleted file]	blob \| history
test/regress/regress0/auflia/Makefile.am		diff \| blob \| history
test/regress/regress0/auflia/bug330.smt2	[deleted file]	blob \| history
test/regress/regress0/bug425.cvc	[deleted file]	blob \| history
test/regress/regress0/bug519.smt2	[deleted file]	blob \| history
test/regress/regress0/bug521.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/bv-proof00.smt	[deleted file]	blob \| history
test/regress/regress0/bv/fuzz34.smt	[deleted file]	blob \| history
test/regress/regress0/bv/fuzz38.smt	[deleted file]	blob \| history
test/regress/regress0/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress0/datatypes/manos-model.smt2	[deleted file]	blob \| history
test/regress/regress0/decision/Makefile.am		diff \| blob \| history
test/regress/regress0/decision/error3.smt	[deleted file]	blob \| history
test/regress/regress0/fmf/ForElimination-scala-9.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/Makefile.am		diff \| blob \| history
test/regress/regress0/lemmas/Makefile.am		diff \| blob \| history
test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt	[deleted file]	blob \| history
test/regress/regress0/lemmas/pursuit-safety-8.smt	[deleted file]	blob \| history
test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt	[deleted file]	blob \| history
test/regress/regress0/rewriterules/Makefile.am		diff \| blob \| history
test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/read5.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/Makefile.am		diff \| blob \| history
test/regress/regress0/sep/loop-1220.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-simp-unc.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/split-find-unsat-w-emp.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/split-find-unsat.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/Makefile.am		diff \| blob \| history
test/regress/regress0/sets/card-vc6-minimized.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/sets-disequal.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/Makefile.am		diff \| blob \| history
test/regress/regress0/strings/cmu-5042-0707-2.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/cmu-dis-0707-3.smt2	[deleted file]	blob \| history
test/regress/regress0/sygus/Makefile.am		diff \| blob \| history
test/regress/regress0/sygus/hd-sdiv.sy	[deleted file]	blob \| history
test/regress/regress1/DTP_k2_n35_c175_s15.smt2	[deleted file]	blob \| history
test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2	[deleted file]	blob \| history
test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect	[deleted file]	blob \| history
test/regress/regress1/GEO123+1.minimized.smt2	[deleted file]	blob \| history
test/regress/regress1/Makefile	[deleted file]	blob \| history
test/regress/regress1/Makefile.am		diff \| blob \| history
test/regress/regress1/arith/Makefile	[deleted file]	blob \| history
test/regress/regress1/arith/Makefile.am	[deleted file]	blob \| history
test/regress/regress1/arith/abz5_1400.smt	[deleted file]	blob \| history
test/regress/regress1/arith/lpsat-goal-9.smt2	[deleted file]	blob \| history
test/regress/regress1/arith/prp-13-24.smt2	[deleted file]	blob \| history
test/regress/regress1/arith/pursuit-safety-11.smt	[deleted file]	blob \| history
test/regress/regress1/arith/pursuit-safety-12.smt	[deleted file]	blob \| history
test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2	[deleted file]	blob \| history
test/regress/regress1/arith/sc-7.base.cvc.smt	[deleted file]	blob \| history
test/regress/regress1/arith/uart-8.base.cvc.smt	[deleted file]	blob \| history
test/regress/regress1/aufbv/fuzz10.smt	[new file with mode: 0644]	blob
test/regress/regress1/auflia-fuzz06.smt	[deleted file]	blob \| history
test/regress/regress1/auflia/bug330.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug136.smt	[deleted file]	blob \| history
test/regress/regress1/bug148.smt	[deleted file]	blob \| history
test/regress/regress1/bug394.smt2	[deleted file]	blob \| history
test/regress/regress1/bug425.cvc	[new file with mode: 0644]	blob
test/regress/regress1/bug519.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug521.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/bv-proof00.smt	[new file with mode: 0644]	blob
test/regress/regress1/bv/fuzz34.smt	[new file with mode: 0644]	blob
test/regress/regress1/bv/fuzz38.smt	[new file with mode: 0644]	blob
test/regress/regress1/datatypes/manos-model.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/error3.smt	[new file with mode: 0644]	blob
test/regress/regress1/error0.smt2	[deleted file]	blob \| history
test/regress/regress1/error1.smt	[deleted file]	blob \| history
test/regress/regress1/fmf/ForElimination-scala-9.smt2	[new file with mode: 0644]	blob
test/regress/regress1/friedman_n4_i5.smt	[deleted file]	blob \| history
test/regress/regress1/fuzz_2.smt	[deleted file]	blob \| history
test/regress/regress1/hash_sat_06_19.smt2	[deleted file]	blob \| history
test/regress/regress1/hash_sat_07_17.smt2	[deleted file]	blob \| history
test/regress/regress1/hash_sat_09_09.smt2	[deleted file]	blob \| history
test/regress/regress1/hash_sat_10_09.smt2	[deleted file]	blob \| history
test/regress/regress1/hole7.cvc	[deleted file]	blob \| history
test/regress/regress1/hole8.cvc	[deleted file]	blob \| history
test/regress/regress1/instance_1444.smt	[deleted file]	blob \| history
test/regress/regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt	[new file with mode: 0644]	blob
test/regress/regress1/lemmas/pursuit-safety-8.smt	[new file with mode: 0644]	blob
test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt	[new file with mode: 0644]	blob
test/regress/regress1/ooo.rf6.smt2	[deleted file]	blob \| history
test/regress/regress1/ooo.tag10.smt2	[deleted file]	blob \| history
test/regress/regress1/piVC_5581bd.smt2	[deleted file]	blob \| history
test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/read5.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/loop-1220.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-simp-unc.smt2	[new file with mode: 0755]	blob
test/regress/regress1/sep/split-find-unsat-w-emp.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/split-find-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/card-vc6-minimized.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/sets-disequal.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/cmu-5042-0707-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/cmu-dis-0707-3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/hd-sdiv.sy	[new file with mode: 0644]	blob
test/regress/regress1/typed_v1l50016-simp.cvc	[deleted file]	blob \| history
test/regress/regress1/uflia-error0.smt2	[deleted file]	blob \| history
test/regress/regress1/uflia-error0.smt2.expect	[deleted file]	blob \| history
test/regress/regress1/xs-09-16-3-4-1-5.decn.smt	[deleted file]	blob \| history
test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect	[deleted file]	blob \| history
test/regress/regress1/xs-09-16-3-4-1-5.smt	[deleted file]	blob \| history
test/regress/regress1/xs-11-20-5-2-5-3.smt	[deleted file]	blob \| history
test/regress/regress1/xs-11-20-5-2-5-3.smt2	[deleted file]	blob \| history
test/regress/regress2/DTP_k2_n35_c175_s15.smt2	[new file with mode: 0644]	blob
test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2	[new file with mode: 0644]	blob
test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress2/GEO123+1.minimized.smt2	[new file with mode: 0644]	blob
test/regress/regress2/Makefile		diff \| blob \| history
test/regress/regress2/Makefile.am		diff \| blob \| history
test/regress/regress2/arith/Makefile	[new file with mode: 0644]	blob
test/regress/regress2/arith/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress2/arith/abz5_1400.smt	[new file with mode: 0644]	blob
test/regress/regress2/arith/lpsat-goal-9.smt2	[new file with mode: 0644]	blob
test/regress/regress2/arith/prp-13-24.smt2	[new file with mode: 0644]	blob
test/regress/regress2/arith/pursuit-safety-11.smt	[new file with mode: 0644]	blob
test/regress/regress2/arith/pursuit-safety-12.smt	[new file with mode: 0644]	blob
test/regress/regress2/arith/qlock-4-10-9.base.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress2/arith/sc-7.base.cvc.smt	[new file with mode: 0644]	blob
test/regress/regress2/arith/uart-8.base.cvc.smt	[new file with mode: 0644]	blob
test/regress/regress2/auflia-fuzz06.smt	[new file with mode: 0644]	blob
test/regress/regress2/bmc-ibm-1.smt	[deleted file]	blob \| history
test/regress/regress2/bmc-ibm-2.smt	[deleted file]	blob \| history
test/regress/regress2/bmc-ibm-5.smt	[deleted file]	blob \| history
test/regress/regress2/bmc-ibm-7.smt	[deleted file]	blob \| history
test/regress/regress2/bug136.smt	[new file with mode: 0644]	blob
test/regress/regress2/bug148.smt	[new file with mode: 0644]	blob
test/regress/regress2/bug394.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bug497.cvc	[deleted file]	blob \| history
test/regress/regress2/eq_diamond14.smt	[deleted file]	blob \| history
test/regress/regress2/error0.smt2	[new file with mode: 0644]	blob
test/regress/regress2/error1.smt	[new file with mode: 0644]	blob
test/regress/regress2/friedman_n4_i5.smt	[new file with mode: 0644]	blob
test/regress/regress2/friedman_n6_i4.smt	[deleted file]	blob \| history
test/regress/regress2/fuzz_2.smt	[new file with mode: 0644]	blob
test/regress/regress2/hash_sat_06_19.smt2	[new file with mode: 0644]	blob
test/regress/regress2/hash_sat_07_17.smt2	[new file with mode: 0644]	blob
test/regress/regress2/hash_sat_09_09.smt2	[new file with mode: 0644]	blob
test/regress/regress2/hash_sat_10_09.smt2	[new file with mode: 0644]	blob
test/regress/regress2/hole7.cvc	[new file with mode: 0644]	blob
test/regress/regress2/hole8.cvc	[new file with mode: 0644]	blob
test/regress/regress2/hole9.cvc	[deleted file]	blob \| history
test/regress/regress2/incorrect1.smt	[deleted file]	blob \| history
test/regress/regress2/incorrect2.smt	[deleted file]	blob \| history
test/regress/regress2/instance_1444.smt	[new file with mode: 0644]	blob
test/regress/regress2/ooo.rf6.smt2	[new file with mode: 0644]	blob
test/regress/regress2/ooo.tag10.smt2	[new file with mode: 0644]	blob
test/regress/regress2/piVC_5581bd.smt2	[new file with mode: 0644]	blob
test/regress/regress2/pp-regfile.smt	[deleted file]	blob \| history
test/regress/regress2/pp-regfile.smt.expect	[deleted file]	blob \| history
test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt	[deleted file]	blob \| history
test/regress/regress2/typed_v1l50016-simp.cvc	[new file with mode: 0644]	blob
test/regress/regress2/uflia-error0.smt2	[new file with mode: 0644]	blob
test/regress/regress2/uflia-error0.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress2/xs-09-16-3-4-1-5.decn.smt	[new file with mode: 0644]	blob
test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect	[new file with mode: 0644]	blob
test/regress/regress2/xs-09-16-3-4-1-5.smt	[new file with mode: 0644]	blob
test/regress/regress2/xs-11-20-5-2-5-3.smt	[new file with mode: 0644]	blob
test/regress/regress2/xs-11-20-5-2-5-3.smt2	[new file with mode: 0644]	blob
test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt	[deleted file]	blob \| history
test/regress/regress3/Makefile		diff \| blob \| history
test/regress/regress3/Makefile.am		diff \| blob \| history
test/regress/regress3/NEQ016_size5.smt	[deleted file]	blob \| history
test/regress/regress3/bmc-ibm-1.smt	[new file with mode: 0644]	blob
test/regress/regress3/bmc-ibm-2.smt	[new file with mode: 0644]	blob
test/regress/regress3/bmc-ibm-5.smt	[new file with mode: 0644]	blob
test/regress/regress3/bmc-ibm-7.smt	[new file with mode: 0644]	blob
test/regress/regress3/bug143.smt	[deleted file]	blob \| history
test/regress/regress3/bug497.cvc	[new file with mode: 0644]	blob
test/regress/regress3/comb2.shuffled-as.sat03-420.smt	[deleted file]	blob \| history
test/regress/regress3/eq_diamond14.smt	[new file with mode: 0644]	blob
test/regress/regress3/friedman_n6_i4.smt	[new file with mode: 0644]	blob
test/regress/regress3/hole10.cvc	[deleted file]	blob \| history
test/regress/regress3/hole9.cvc	[new file with mode: 0644]	blob
test/regress/regress3/incorrect1.smt	[new file with mode: 0644]	blob
test/regress/regress3/incorrect2.smt	[new file with mode: 0644]	blob
test/regress/regress3/instance_1151.smt	[deleted file]	blob \| history
test/regress/regress3/pp-regfile.smt	[new file with mode: 0644]	blob
test/regress/regress3/pp-regfile.smt.expect	[new file with mode: 0644]	blob
test/regress/regress3/qwh.35.405.shuffled-as.sat03-1651.smt	[new file with mode: 0644]	blob
test/regress/regress4/C880mul.miter.shuffled-as.sat03-348.smt	[new file with mode: 0644]	blob
test/regress/regress4/Makefile	[new file with mode: 0644]	blob
test/regress/regress4/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress4/NEQ016_size5.smt	[new file with mode: 0644]	blob
test/regress/regress4/bug143.smt	[new file with mode: 0644]	blob
test/regress/regress4/comb2.shuffled-as.sat03-420.smt	[new file with mode: 0644]	blob
test/regress/regress4/hole10.cvc	[new file with mode: 0644]	blob
test/regress/regress4/instance_1151.smt	[new file with mode: 0644]	blob

RSS Atom