2 files changed, 0 insertions, 42 deletions
diff --git a/Test/aitest9/answer b/Test/aitest9/answer
deleted file mode 100644
index ef9f4d83..00000000
--- a/Test/aitest9/answer
+++ /dev/null
@@ -1,31 +0,0 @@
- 
--------------------- VarMapFixPoint.bpl -------------------- 
-VarMapFixPoint.bpl(13,5): Error BP5005: This loop invariant might not be maintained by the loop.
-Execution trace:
-    VarMapFixPoint.bpl(7,3): start
-    VarMapFixPoint.bpl(12,3): LoopHead
-    VarMapFixPoint.bpl(16,3): LoopBody
-
-Boogie program verifier finished with 1 verified, 1 error
- 
--------------------- TestIntervals.bpl -------------------- 
-TestIntervals.bpl(25,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    TestIntervals.bpl(7,5): anon0
-    TestIntervals.bpl(8,3): anon9_LoopHead
-    TestIntervals.bpl(14,14): anon10_Then
-    TestIntervals.bpl(15,14): anon11_Then
-    TestIntervals.bpl(16,14): anon12_Then
-    TestIntervals.bpl(19,5): anon8
-TestIntervals.bpl(70,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    TestIntervals.bpl(62,3): anon0
-    TestIntervals.bpl(67,3): anon3_LoopHead
-    TestIntervals.bpl(67,3): anon3_LoopDone
-TestIntervals.bpl(71,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    TestIntervals.bpl(62,3): anon0
-    TestIntervals.bpl(67,3): anon3_LoopHead
-    TestIntervals.bpl(67,3): anon3_LoopDone
-
-Boogie program verifier finished with 2 verified, 3 errors
diff --git a/Test/aitest9/runtest.bat b/Test/aitest9/runtest.bat
deleted file mode 100644
index e66f7e2b..00000000
--- a/Test/aitest9/runtest.bat
+++ /dev/null
@@ -1,11 +0,0 @@
-@echo off
-setlocal
-
-set BOOGIEDIR=..\..\Binaries
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-
-for %%f in (VarMapFixPoint.bpl TestIntervals.bpl) do (
-  echo. 
-  echo -------------------- %%f -------------------- 
-  %BPLEXE% %* %%f /infer:j
-)