From 4a39e65198a98e148403e59473cede4895c7d2e7 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Fri, 30 Sep 2011 15:02:27 -0700
Subject: bug fix in houdini also fixed runtest.bat and Answer

---
 Test/houdini/Answer      | 30 ------------------------------
 Test/houdini/runtest.bat |  2 +-
 2 files changed, 1 insertion(+), 31 deletions(-)

(limited to 'Test/houdini')

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 8c0f30ea..d29caa5c 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -4,14 +4,6 @@
 Boogie program verifier finished with 1 verified, 0 errors
 
 -------------------- houd2.bpl --------------------
-----------------------------------------
-Functions: Errors
-	bar
-----------------------------------------
-houd2.bpl(12,1): Error BP5003: A postcondition might not hold at this return statement.
-houd2.bpl(9,1): Related location: This is the postcondition that might not hold.
-Execution trace:
-    houd2.bpl(11,3): anon0
 
 Boogie program verifier finished with 1 verified, 1 error
 
@@ -40,36 +32,14 @@ Boogie program verifier finished with 2 verified, 0 errors
 Boogie program verifier finished with 1 verified, 0 errors
 
 -------------------- houd9.bpl --------------------
-----------------------------------------
-Functions: Errors
-	foo
-----------------------------------------
-houd9.bpl(19,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    houd9.bpl(18,9): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
 
 -------------------- houd10.bpl --------------------
-----------------------------------------
-Functions: Errors
-	foo
-----------------------------------------
-houd10.bpl(15,3): Error BP5002: A precondition for this call might not hold.
-houd10.bpl(20,1): Related location: This is the precondition that might not hold.
-Execution trace:
-    houd10.bpl(14,9): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
 
 -------------------- houd11.bpl --------------------
-----------------------------------------
-Functions: Errors
-	foo
-----------------------------------------
-houd11.bpl(8,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    houd11.bpl(7,9): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
 
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index ae82455a..2a391b2c 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -6,6 +6,6 @@ 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 /prover:z3 /Houdini:ci %%f
+  %BGEXE% %* /nologo /contractInfer %%f
 rem  %BGEXE% %* /nologo /prover:z3api /Houdini:ci %%f
 )
-- 
cgit v1.2.3