diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-16 15:40:46 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-16 15:40:46 -0800 |
| commit | e611277c4d889de2db5d27c54eb64e149c3f194d (patch) | |
| tree | 35ef9f0044361523953db23c6734188b0ef6451d | |
| parent | 7c4a89d9adbe8b8779d3691273ee407655754d3f (diff) | |
/contractInfer always prints the computed assignment now
enabled the houdini regressions
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 8 | ||||
| -rw-r--r-- | Test/houdini/Answer | 53 | ||||
| -rw-r--r-- | Test/houdini/runtest.bat | 3 |
3 files changed, 57 insertions, 7 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 028ff1dd..7b5576c1 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -440,11 +440,9 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.ContractInfer) {
Houdini.Houdini houdini = new Houdini.Houdini(program, true);
Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment) {
- Console.WriteLine(x.Key + " = " + x.Value);
- }
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment) {
+ Console.WriteLine(x.Key + " = " + x.Value);
}
errorCount = outcome.ErrorCount;
verified = outcome.Verified;
diff --git a/Test/houdini/Answer b/Test/houdini/Answer index d29caa5c..94ae7f04 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -1,48 +1,101 @@ -------------------- houd1.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd2.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = True
Boogie program verifier finished with 1 verified, 1 error
-------------------- houd3.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = False
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd4.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
+b4 = True
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd5.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = True
+b3 = False
+b4 = True
+b5 = True
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd6.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = False
+b3 = False
+b4 = False
+b5 = False
+b6 = False
+b7 = False
+b8 = False
Boogie program verifier finished with 3 verified, 0 errors
-------------------- houd7.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = False
+b3 = False
Boogie program verifier finished with 2 verified, 0 errors
-------------------- houd8.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = False
+b3 = False
Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd9.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
Boogie program verifier finished with 0 verified, 1 error
-------------------- houd10.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
Boogie program verifier finished with 0 verified, 1 error
-------------------- houd11.bpl --------------------
+Assignment computed by Houdini:
Boogie program verifier finished with 0 verified, 1 error
-------------------- houd12.bpl --------------------
+Assignment computed by Houdini:
+b1 = False
+b2 = True
+b3 = True
+b4 = True
+b5 = True
+b6 = False
+b7 = False
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat index 2a391b2c..d0e53b08 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -6,6 +6,5 @@ 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 /contractInfer %%f
-rem %BGEXE% %* /nologo /prover:z3api /Houdini:ci %%f
+ %BGEXE% %* /nologo /noinfer /contractInfer %%f
)
|