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 /Source/BoogieDriver | |
| parent | 7c4a89d9adbe8b8779d3691273ee407655754d3f (diff) | |
/contractInfer always prints the computed assignment now
enabled the houdini regressions
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 8 |
1 files changed, 3 insertions, 5 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;
|