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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 9 Dec 2020 09:57:13 +0000 (03:57 -0600)
committer	GitHub <noreply@github.com>
	Wed, 9 Dec 2020 09:57:13 +0000 (10:57 +0100)
commit	59cd96a33b8f32405be2a20fc8230efc33b8dcdc
tree	ad6d9b97c1a1da7026e84500f0b2ffe6081a17de	tree
parent	adc9bb5dff0c3d705b91d862d61a0c3057350688	commit \| diff

Remove obsolete regressions (#5633)

This removes benchmarks for the following reasons:

- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed

145 files changed:

test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/bv/core/concat-merge-0.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/concat-merge-1.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/concat-merge-2.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/concat-merge-3.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/equality-00.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/equality-01.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/equality-02.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/equality-03.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/equality-03.smtv1.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-0.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-1.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-10.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-11.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-2.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-3.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-4.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-5.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-6.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-7.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-8.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-concat-9.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-constant.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-0.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-1.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-10.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-11.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-2.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-3.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-4.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-5.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-6.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-7.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-8.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-extract-9.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-whole-0.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-whole-1.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-whole-2.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-whole-3.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/extract-whole-4.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-01.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-02.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-03.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-04.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-05.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-06.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-07.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-08.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-09.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-10.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-11.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-12.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-13.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-14.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-15.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-16.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-17.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-18.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-19.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/core/slice-20.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-001.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-002.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-003.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-005.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-006.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-007.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-008.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-009.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-010.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-016.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-017.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-018.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-019.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-020.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-026.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-027.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-028.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-029.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-030.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-031.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-032.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-033.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-034.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-035.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-036.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-037.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-038.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-039.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-040.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-041.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-043.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-044.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-045.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-046.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-049.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-051.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-052.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-053.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-054.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-055.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-056.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-057.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-058.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-059.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-060.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-061.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-062.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-063.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-064.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-065.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-066.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-067.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-068.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-069.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-070.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-071.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-072.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-073.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-074.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-075.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-076.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-077.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-078.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-080.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-081.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-082.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-083.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-086.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-087.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-088.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-089.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-090.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-091.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-092.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-093.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-094.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-095.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-096.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-099.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-100.cvc	[deleted file]	blob \| history
test/regress/regress1/bug585.cvc	[deleted file]	blob \| history
test/regress/regress1/crash_burn_locusts.smt2	[deleted file]	blob \| history
test/regress/regress1/issue1048-arrays-int-real.smt2	[deleted file]	blob \| history
test/regress/regress1/sygus/enum-test.sy	[deleted file]	blob \| history

RSS Atom