From 7d1a42f0c26e2c7ba37a7de4b1ba3175777596c9 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Fri, 2 Mar 2012 11:28:04 -0800
Subject: various refactorings related to houdini

---
 Test/houdini/Answer      | 14 ++++++++++++++
 Test/houdini/runtest.bat |  4 ++--
 2 files changed, 16 insertions(+), 2 deletions(-)

(limited to 'Test')

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 6053b442..d7edbce6 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -9,6 +9,10 @@ Boogie program verifier finished with 1 verified, 0 errors
 Assignment computed by Houdini:
 b1 = False
 b2 = True
+houd2.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+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
 
@@ -72,6 +76,9 @@ Assignment computed by Houdini:
 b1 = True
 b2 = True
 b3 = True
+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
 
@@ -80,11 +87,18 @@ Assignment computed by Houdini:
 b1 = True
 b2 = True
 b3 = True
+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 --------------------
 Assignment computed by Houdini:
+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 f0065b0d..b9816bb9 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -6,11 +6,11 @@ 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 %%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 /inlineDepth:1 %%f
+  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f
 )
-- 
cgit v1.2.3