Removed old test infrastructure files except for

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

because their conversion to lit incomplete.

2 files changed, 0 insertions, 132 deletions

diff --git a/Test/og/Answer b/Test/og/Answer
deleted file mode 100644
index 4b1bceae..00000000
--- a/Test/og/Answer
+++ /dev/null
@@ -1,115 +0,0 @@
-

--------------------- foo.bpl --------------------

-foo.bpl(30,3): Error: Non-interference check failed

-Execution trace:

-    foo.bpl(7,3): anon0

-    foo.bpl(7,3): anon0$1

-    foo.bpl(14,3): inline$Incr_1$0$this_A

-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

-

-Boogie program verifier finished with 9 verified, 1 error

-

--------------------- bar.bpl --------------------

-bar.bpl(28,3): Error: Non-interference check failed

-Execution trace:

-    bar.bpl(7,3): anon0

-    bar.bpl(7,3): anon0$1

-    bar.bpl(14,3): inline$Incr_1$0$this_A

-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

-bar.bpl(28,3): Error: Non-interference check failed

-Execution trace:

-    bar.bpl(38,3): anon0

-    bar.bpl(38,3): anon0$1

-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

-

-Boogie program verifier finished with 8 verified, 2 errors

-

--------------------- one.bpl --------------------

-

-Boogie program verifier finished with 3 verified, 0 errors

-

--------------------- parallel1.bpl --------------------

-parallel1.bpl(30,3): Error: Non-interference check failed

-Execution trace:

-    parallel1.bpl(7,3): anon0

-    parallel1.bpl(7,3): anon0$1

-    parallel1.bpl(14,3): inline$Incr_1$0$this_A

-    (0,0): inline$Impl_YieldChecker_PC_1$1$L0

-

-Boogie program verifier finished with 7 verified, 1 error

-

--------------------- linear-set.bpl --------------------

-

-Boogie program verifier finished with 4 verified, 0 errors

-

--------------------- linear-set2.bpl --------------------

-

-Boogie program verifier finished with 4 verified, 0 errors

-

--------------------- FlanaganQadeer.bpl --------------------

-

-Boogie program verifier finished with 6 verified, 0 errors

-

--------------------- parallel2.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

--------------------- parallel4.bpl --------------------

-parallel4.bpl(26,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    (0,0): og_init

-    parallel4.bpl(24,5): anon0$1

-

-Boogie program verifier finished with 5 verified, 1 error

-

--------------------- parallel5.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

--------------------- akash.bpl --------------------

-

-Boogie program verifier finished with 6 verified, 0 errors

-

--------------------- t1.bpl --------------------

-t1.bpl(60,5): Error: Non-interference check failed

-Execution trace:

-    (0,0): og_init

-    t1.bpl(80,13): anon0

-    t1.bpl(80,13): anon0$1

-    (0,0): inline$SetG_1$0$Entry

-    t1.bpl(80,13): anon0$2

-    (0,0): inline$Impl_YieldChecker_A_1$1$L2

-

-Boogie program verifier finished with 5 verified, 1 error

-

--------------------- new1.bpl --------------------

-

-Boogie program verifier finished with 4 verified, 0 errors

-

--------------------- perm.bpl --------------------

-

-Boogie program verifier finished with 4 verified, 0 errors

-

--------------------- DeviceCache.bpl --------------------

-

-Boogie program verifier finished with 35 verified, 0 errors

-

--------------------- ticket.bpl --------------------

-

-Boogie program verifier finished with 28 verified, 0 errors

-

--------------------- lock.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

--------------------- lock2.bpl --------------------

-

-Boogie program verifier finished with 8 verified, 0 errors

-

--------------------- multiset.bpl --------------------

-

-Boogie program verifier finished with 85 verified, 0 errors

-

--------------------- civl-paper.bpl --------------------

-

-Boogie program verifier finished with 28 verified, 0 errors

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

-setlocal

-

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

-

-for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (

-  echo.

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

-  %BGEXE% %* /nologo /noinfer %%f

-)

-

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl civl-paper.bpl) do (

-  echo.

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

-  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

-)

-