diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-18 22:09:07 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-18 22:09:07 -0800 |
| commit | 24ccf275b190b71b671e1884a58e83fe0976f4d3 (patch) | |
| tree | ab61b65851a097c79eb41c89054ffa17dbb578b6 /Test/houdini | |
| parent | 1d7648ed968a478e03900c18ecd43f5b1443457c (diff) | |
fixed a completeness problem in houdini with inlining
Diffstat (limited to 'Test/houdini')
| -rw-r--r-- | Test/houdini/Answer | 9 | ||||
| -rw-r--r-- | Test/houdini/runtest.bat | 2 |
2 files changed, 10 insertions, 1 deletions
diff --git a/Test/houdini/Answer b/Test/houdini/Answer index b8e22af3..6053b442 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -146,3 +146,12 @@ 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 index de2e6099..f0065b0d 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -9,7 +9,7 @@ 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 test9.bpl) do (
+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
|