Removed old test infrastructure files except for

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

because their conversion to lit incomplete.

2 files changed, 0 insertions, 187 deletions

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
deleted file mode 100644
index a5eab2fe..00000000
--- a/Test/houdini/Answer
+++ /dev/null
@@ -1,171 +0,0 @@
-

--------------------- houd1.bpl --------------------

-Assignment computed by Houdini:

-b1 = False

-

-Boogie program verifier finished with 1 verified, 0 errors

-

--------------------- houd2.bpl --------------------

-Assignment computed by Houdini:

-b1 = False

-b2 = True

-houd2.bpl(14,1): Error BP5003: A postcondition might not hold on this return path.

-houd2.bpl(11,1): Related location: This is the postcondition that might not hold.

-Execution trace:

-    houd2.bpl(13,3): anon0

-

-Boogie program verifier finished with 1 verified, 1 error

-

--------------------- houd3.bpl --------------------

-Assignment computed by Houdini:

-b1 = False

-b2 = False

-

-Boogie program verifier finished with 2 verified, 0 errors

-

--------------------- houd4.bpl --------------------

-Assignment computed by Houdini:

-b1 = True

-b2 = True

-b3 = True

-b4 = True

-

-Boogie program verifier finished with 2 verified, 0 errors

-

--------------------- houd5.bpl --------------------

-Assignment computed by Houdini:

-b1 = False

-b2 = True

-b3 = False

-b4 = True

-b5 = True

-

-Boogie program verifier finished with 2 verified, 0 errors

-

--------------------- houd6.bpl --------------------

-Assignment computed by Houdini:

-b1 = False

-b2 = False

-b3 = False

-b4 = False

-b5 = False

-b6 = False

-b7 = False

-b8 = False

-

-Boogie program verifier finished with 3 verified, 0 errors

-

--------------------- houd7.bpl --------------------

-Assignment computed by Houdini:

-b1 = True

-b2 = False

-b3 = False

-

-Boogie program verifier finished with 2 verified, 0 errors

-

--------------------- houd8.bpl --------------------

-Assignment computed by Houdini:

-b1 = True

-b2 = False

-b3 = False

-

-Boogie program verifier finished with 1 verified, 0 errors

-

--------------------- houd9.bpl --------------------

-Assignment computed by Houdini:

-b1 = True

-b2 = True

-b3 = True

-houd9.bpl(21,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    houd9.bpl(20,9): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- houd10.bpl --------------------

-Assignment computed by Houdini:

-b1 = True

-b2 = True

-b3 = True

-houd10.bpl(17,3): Error BP5002: A precondition for this call might not hold.

-houd10.bpl(22,1): Related location: This is the precondition that might not hold.

-Execution trace:

-    houd10.bpl(16,9): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- houd11.bpl --------------------

-Assignment computed by Houdini:

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

-Execution trace:

-    houd11.bpl(9,9): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- houd12.bpl --------------------

-Assignment computed by Houdini:

-b1 = False

-b2 = True

-b3 = True

-b4 = True

-b5 = True

-b6 = False

-b7 = False

-

-Boogie program verifier finished with 1 verified, 0 errors

-.

--------------------- test1.bpl --------------------

-Assignment computed by Houdini:

-b0 = True

-b1 = False

-b2 = False

-

-Boogie program verifier finished with 4 verified, 0 errors

-.

--------------------- test2.bpl --------------------

-Assignment computed by Houdini:

-b0 = True

-b1 = False

-b2 = False

-

-Boogie program verifier finished with 4 verified, 0 errors

-.

--------------------- test7.bpl --------------------

-Assignment computed by Houdini:

-

-Boogie program verifier finished with 2 verified, 0 errors

-.

--------------------- test8.bpl --------------------

-Assignment computed by Houdini:

-

-Boogie program verifier finished with 2 verified, 0 errors

-.

--------------------- test9.bpl --------------------

-Assignment computed by Houdini:

-b1 = False

-b2 = False

-b3 = False

-b4 = True

-b5 = False

-b6 = True

-b7 = False

-b8 = False

-b9 = False

-b10 = True

-b11 = False

-b12 = True

-b13 = False

-b14 = False

-b15 = False

-b16 = False

-

-Boogie program verifier finished with 5 verified, 0 errors

-.

--------------------- test10.bpl --------------------

-Assignment computed by Houdini:

-b1 = True

-b2 = True

-b3 = True

-b4 = True

-

-Boogie program verifier finished with 5 verified, 0 errors

diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
deleted file mode 100644
index b9816bb9..00000000
--- a/Test/houdini/runtest.bat
+++ /dev/null
@@ -1,16 +0,0 @@
-@echo off

-setlocal

-

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

-

-for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (

-  echo.

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

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

-)

-

-for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (

-  echo .

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

-  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f

-)