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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 10 Dec 2020 15:09:05 +0000 (09:09 -0600)
committer	GitHub <noreply@github.com>
	Thu, 10 Dec 2020 15:09:05 +0000 (09:09 -0600)
commit	37f51226cc8a96fc699648068f8c72a2f0832f51
tree	5f1ad22a455622b14e331dba112b2b9110ad0b66	tree
parent	ad8d70c5481266a58ceefe41fc0ec46083ba5d6e	commit \| diff

Refactor regressions (#5639)

This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory.

It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+).

101 files changed:

test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/arith/miplib-pp08a-3000.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/aufbv/bug348.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/aufbv/bug349.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/aufbv/bug493.smtv1.smt2		diff \| blob \| history
test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2		diff \| blob \| history
test/regress/regress0/aufbv/wchains010ue.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bug2.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bug374.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/bug345.smtv1.smt2		diff \| blob \| history
test/regress/regress0/bv/core/bitvec0.delta01.smtv1.smt2		diff \| blob \| history
test/regress/regress0/bv/core/equality-05.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/ext_con_004_001_1024.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/core/incremental.smtv1.smt2		diff \| blob \| history
test/regress/regress0/bv/fuzz07-delta.smtv1.smt2		diff \| blob \| history
test/regress/regress0/bv/fuzz15.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/fuzz16.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/fuzz17.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/incorrect1.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/decision/wchains010ue.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/incorrect1.smtv1.smt2		diff \| blob \| history
test/regress/regress0/lemmas/fischer3-mutex-16.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/issue4476-ext-rew.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2		diff \| blob \| history
test/regress/regress0/strings/bidir_star.smt2	[deleted file]	blob \| history
test/regress/regress0/uf/PEQ018_size4.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/diseqprop.01.smtv1.smt2		diff \| blob \| history
test/regress/regress0/uflia/diseqprop.02.smtv1.smt2		diff \| blob \| history
test/regress/regress0/uflia/diseqprop.03.smtv1.smt2		diff \| blob \| history
test/regress/regress0/uflia/diseqprop.04.smtv1.smt2		diff \| blob \| history
test/regress/regress0/uflia/diseqprop.05.smtv1.smt2		diff \| blob \| history
test/regress/regress0/uflia/diseqprop.06.smtv1.smt2		diff \| blob \| history
test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2		diff \| blob \| history
test/regress/regress1/aufbv/bug348.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/auflia/bug337.smt2	[deleted file]	blob \| history
test/regress/regress1/bug590.smt2		diff \| blob \| history
test/regress/regress1/bv/incorrect1.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/issue3803-nl-check-model.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/arith-snorm.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue4476-ext-rew.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rr-verify/regex.sy	[deleted file]	blob \| history
test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/cegisunif-depth1.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/interpol2.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy	[deleted file]	blob \| history
test/regress/regress2/arith/lpsat-goal-9.smt2	[deleted file]	blob \| history
test/regress/regress2/arith/miplib-pp08a-3000.smt2	[deleted file]	blob \| history
test/regress/regress2/auflia-fuzz06.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress2/bug349.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bug374.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bug396.smt2	[deleted file]	blob \| history
test/regress/regress2/hole10.cvc	[new file with mode: 0644]	blob
test/regress/regress2/nl/dumortier-050317.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2	[deleted file]	blob \| history
test/regress/regress2/strings/bidir_star.smt2	[new file with mode: 0644]	blob
test/regress/regress2/sygus/DRAGON_1.lus.sy	[deleted file]	blob \| history
test/regress/regress2/sygus/inv_gen_n_c11.sy	[deleted file]	blob \| history
test/regress/regress2/sygus/nia-max-square.sy	[deleted file]	blob \| history
test/regress/regress2/sygus/policyM.sy	[deleted file]	blob \| history
test/regress/regress2/sygus/vcb.sy	[deleted file]	blob \| history
test/regress/regress2/xs-11-20-5-2-5-3.smt2	[deleted file]	blob \| history
test/regress/regress2/xs-11-20-5-2-5-3.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress3/DRAGON_1.lus.sy	[new file with mode: 0644]	blob
test/regress/regress3/PEQ018_size4.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/aufbv-wchains010ue.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/auflia-fuzz06.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/bug2.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/bv-core-ext_con_004_001_1024.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/bv-fuzz15.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/bv-fuzz16.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/bv-fuzz17.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/cegisunif-depth1.sy	[new file with mode: 0644]	blob
test/regress/regress3/decision-uflia-xs-09-16-3-4-1-5.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/decision-wchains010ue.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress3/interpol2.smt2	[new file with mode: 0644]	blob
test/regress/regress3/inv_gen_n_c11.sy	[new file with mode: 0644]	blob
test/regress/regress3/issue2429.smt2	[deleted file]	blob \| history
test/regress/regress3/lpsat-goal-9.smt2	[new file with mode: 0644]	blob
test/regress/regress3/nia-max-square.sy	[new file with mode: 0644]	blob
test/regress/regress3/policyM.sy	[new file with mode: 0644]	blob
test/regress/regress3/pp-regfile.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress3/regex-rrv.sy	[new file with mode: 0644]	blob
test/regress/regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2	[new file with mode: 0644]	blob
test/regress/regress3/strings/unsat-circ-reduce.smt2	[deleted file]	blob \| history
test/regress/regress3/unbdd_inv_gen_ex7.sy	[new file with mode: 0644]	blob
test/regress/regress3/unifpi-solve-car_1.lus.sy	[new file with mode: 0644]	blob
test/regress/regress3/vcb.sy	[new file with mode: 0644]	blob
test/regress/regress4/bug337.smt2	[new file with mode: 0644]	blob
test/regress/regress4/bug396.smt2	[new file with mode: 0644]	blob
test/regress/regress4/fischer3-mutex-16.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress4/hole10.cvc	[deleted file]	blob \| history
test/regress/regress4/issue2429.smt2	[new file with mode: 0644]	blob
test/regress/regress4/miplib-pp08a-3000.smt2	[new file with mode: 0644]	blob
test/regress/regress4/miplib-pp08a-3000.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress4/pp-regfile.smtv1.smt2	[new file with mode: 0644]	blob
test/regress/regress4/sets-card-neg-mem-union-2.smt2	[new file with mode: 0644]	blob
test/regress/regress4/unsat-circ-reduce.smt2	[new file with mode: 0644]	blob
test/regress/regress4/xs-11-20-5-2-5-3.smt2	[new file with mode: 0644]	blob
test/regress/regress4/xs-11-20-5-2-5-3.smtv1.smt2	[new file with mode: 0644]	blob

RSS Atom