Removed old test infrastructure files except for

./AbsHoudini/
./doomed/
./z3api/
./test17/

because their conversion to lit incomplete.

2 files changed, 0 insertions, 68 deletions

diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer
deleted file mode 100644
index 6aa2bce2..00000000
--- a/Test/bitvectors/Answer
+++ /dev/null
@@ -1,51 +0,0 @@
--------------------- arrays.bpl --------------------

-

-Boogie program verifier finished with 2 verified, 0 errors

--------------------- bv0.bpl --------------------

-bv0.bpl(6,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32)

-bv0.bpl(7,3): Error: mismatched types in assignment command (cannot assign int to bv32)

-bv0.bpl(8,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)

-bv0.bpl(9,10): Error: start index in extract must be no bigger than the end index

-bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)

-bv0.bpl(11,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32)

-bv0.bpl(12,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32)

-7 type checking errors detected in bv0.bpl

--------------------- bv1.bpl --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

--------------------- bv2.bpl --------------------

-bv2.bpl(6,13): Error: bitvector bounds in illegal position

-bv2.bpl(8,13): Error: undeclared type: x

-bv2.bpl(9,14): Error: bitvector bounds in illegal position

-3 name resolution errors detected in bv2.bpl

--------------------- bv3.bpl --------------------

-bv3.bpl(4,5): Error: type name: bv16 is registered for bitvectors

-1 name resolution errors detected in bv3.bpl

--------------------- bv4.bpl --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

--------------------- bv7.bpl --------------------

-bv7.bpl(6,14): error: arguments of extract need to be integer literals

-bv7.bpl(7,15): error: parentheses around bitvector bounds are not allowed

-2 parse errors detected in bv7.bpl

--------------------- bv5.bpl --------------------

-bv5.bpl(12,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    bv5.bpl(7,12): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

--------------------- bv6.bpl --------------------

-bv6.bpl(10,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    bv6.bpl(7,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

--------------------- bv8.bpl --------------------

-

-Boogie program verifier finished with 2 verified, 0 errors

--------------------- bv10.bpl --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

--------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------

-

-Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat
deleted file mode 100644
index 2a140368..00000000
--- a/Test/bitvectors/runtest.bat
+++ /dev/null
@@ -1,17 +0,0 @@
-@echo off

-setlocal

-

-set BGEXE=..\..\Binaries\Boogie.exe

-

-for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do (

-  echo -------------------- %%f --------------------

-  %BGEXE% /proverWarnings:1 %* %%f

-)

-

-for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do (

-  echo -------------------- %%f --------------------

-  %BGEXE% %* %%f

-)

-

-echo -------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------

-%BGEXE% /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl