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/houdini/Answer      | 171 -----------------------------------------------
 Test/houdini/runtest.bat |  16 -----
 2 files changed, 187 deletions(-)
 delete mode 100644 Test/houdini/Answer
 delete mode 100644 Test/houdini/runtest.bat

(limited to 'Test/houdini')

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