From 08e1dc93d185e221b65bd59ccc167526937ee4d4 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 28 May 2014 16:32:14 +0100
Subject: Removed old test infrastructure files except for

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

because their conversion to lit incomplete.
---
 Test/aitest9/answer      | 31 -------------------------------
 Test/aitest9/runtest.bat | 11 -----------
 2 files changed, 42 deletions(-)
 delete mode 100644 Test/aitest9/answer
 delete mode 100644 Test/aitest9/runtest.bat

(limited to 'Test/aitest9')

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
-)
-- 
cgit v1.2.3