Removed old test infrastructure files except for

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

because their conversion to lit incomplete.

2 files changed, 0 insertions, 157 deletions

diff --git a/Test/test15/Answer b/Test/test15/Answer
deleted file mode 100644
index 7a5cb92f..00000000
--- a/Test/test15/Answer
+++ /dev/null
@@ -1,136 +0,0 @@
-

--------------------- NullInModel --------------------

-*** MODEL

-%lbl%@47 -> false

-%lbl%+24 -> true

-%lbl%+37 -> true

-null -> T@ref!val!0

-s -> T@ref!val!0

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

-}

-*** END_MODEL

-NullInModel.bpl(4,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    NullInModel.bpl(4,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- IntInModel --------------------

-*** MODEL

-%lbl%@39 -> false

-%lbl%+23 -> true

-%lbl%+29 -> true

-i -> 0

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

-}

-*** END_MODEL

-IntInModel.bpl(4,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    IntInModel.bpl(4,3): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- ModelTest --------------------

-*** MODEL

-%lbl%@147 -> false

-%lbl%+64 -> true

-%lbl%+84 -> true

-i@0 -> 1

-j@0 -> 2

-j@1 -> 3

-j@2 -> 4

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

-}

-*** END_MODEL

-ModelTest.bpl(9,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    ModelTest.bpl(5,5): anon0

-

-Boogie program verifier finished with 0 verified, 1 error

-

--------------------- InterpretedFunctionTests --------------------

-InterpretedFunctionTests.bpl(6,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterpretedFunctionTests.bpl(4,3): anon0

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

-Execution trace:

-    InterpretedFunctionTests.bpl(10,3): anon0

-InterpretedFunctionTests.bpl(18,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    InterpretedFunctionTests.bpl(16,3): anon0

-

-Boogie program verifier finished with 0 verified, 3 errors

-

--------------------- CaptureState --------------------

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

-CaptureState.bpl(10,3): Related location: This is the postcondition that might not hold.

-Execution trace:

-    CaptureState.bpl(14,3): anon0

-    CaptureState.bpl(18,5): anon4_Then

-    CaptureState.bpl(26,5): anon3

-*** MODEL

-$mv_state_const -> 3

-%lbl%@293 -> false

-%lbl%+112 -> true

-%lbl%+114 -> true

-%lbl%+118 -> true

-%lbl%+148 -> true

-F -> T@FieldName!val!0

-Heap -> T@[Ref,FieldName]Int!val!0

-m -> **m

-m@0 -> -276

-m@1 -> -275

-m@3 -> -275

-r -> **r

-r@0 -> -550

-this -> T@Ref!val!0

-x -> 719

-y -> **y

-Select_[Ref,FieldName]$int -> {

-  T@[Ref,FieldName]Int!val!0 T@Ref!val!0 T@FieldName!val!0 -> -276

-  else -> -276

-}

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

-}

-$mv_state -> {

-  3 0 -> true

-  3 1 -> true

-  3 2 -> true

-  3 5 -> true

-  else -> true

-}

-*** STATE <initial>

-  Heap -> T@[Ref,FieldName]Int!val!0

-  this -> T@Ref!val!0

-  x -> 719

-  y -> **y

-  r -> **r

-  m -> **m

-*** END_STATE

-*** STATE top

-*** END_STATE

-*** STATE then

-  m -> -276

-*** END_STATE

-*** STATE postUpdate0

-  m -> -275

-*** END_STATE

-*** STATE end

-  r -> -550

-  m -> 7

-*** END_STATE

-*** END_MODEL

-

-Boogie program verifier finished with 0 verified, 1 error

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

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set BGEXE=%BOOGIEDIR%\boogie.exe

-

-for %%f in (NullInModel IntInModel ModelTest) do (

-  echo.

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

-  "%BGEXE%" %* %%f.bpl /printModel:2

-)

-for %%f in (InterpretedFunctionTests) do (

-  echo.

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

-  "%BGEXE%" %* %%f.bpl

-)

-for %%f in (CaptureState) do (

-  echo.

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

-  "%BGEXE%" %* %%f.bpl /mv:-

-)