diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-09-27 21:31:50 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-09-27 21:31:50 -0700 |
| commit | 793059b23a2f3703621dcc9105be160c74e38791 (patch) | |
| tree | 38e5a017edf8e437d232c08f9a008080ff086b89 /Source/BoogieDriver | |
| parent | 811b680ba5dfdbbe495729f7e6dcf024f3c4aabe (diff) | |
updated Houdini so it works with SMTLib
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 8262f749..5a1f8dc5 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -439,9 +439,11 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.ContractInfer) {
Houdini.Houdini houdini = new Houdini.Houdini(program, true);
Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment) {
- Console.WriteLine(x.Key + " = " + x.Value);
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment) {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
}
errorCount = outcome.ErrorCount;
verified = outcome.Verified;
|