diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-05 12:49:13 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-05 12:49:13 -0800 |
| commit | dc96968bfaab78995a6a54e6960a942b804dfe18 (patch) | |
| tree | 12ba0bb1e8da12d23fcc2d932f029772a18e4254 /Test | |
| parent | 4266ee07457dfacdee4f037f4907b4db1758bfec (diff) | |
further fixes to houdini
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/houdini/Answer | 23 | ||||
| -rw-r--r-- | Test/houdini/runtest.bat | 4 |
2 files changed, 24 insertions, 3 deletions
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
)
|