From dc96968bfaab78995a6a54e6960a942b804dfe18 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Mon, 5 Dec 2011 12:49:13 -0800
Subject: further fixes to houdini

---
 Test/houdini/Answer      | 23 ++++++++++++++++++++++-
 Test/houdini/runtest.bat |  4 ++--
 2 files changed, 24 insertions(+), 3 deletions(-)

(limited to 'Test/houdini')

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 474d1b09..b8e22af3 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -124,4 +124,25 @@ Boogie program verifier finished with 2 verified, 0 errors
 -------------------- test8.bpl --------------------
 Assignment computed by Houdini:
 
-Boogie program verifier finished with 3 verified, 0 errors
+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
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index aeffcd12..de2e6099 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -9,8 +9,8 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp
   %BGEXE% %* /nologo /noinfer /contractInfer %%f
 )
 
-for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl) do (
+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl) do (
   echo .
   echo -------------------- %%f --------------------
-  %BGEXE% %* /nologo /noinfer /contractInfer /inline:spec /inlineDepth:1 %%f
+  %BGEXE% %* /nologo /noinfer /contractInfer /inlineDepth:1 %%f
 )
-- 
cgit v1.2.3