diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-08-04 21:55:13 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-08-04 21:55:13 -0700 |
| commit | e129afe1528a5213c56171dd12afaadb1e219d4c (patch) | |
| tree | b55bfba6282f395c2211a90f59a30e2bad87fa27 /Source/BoogieDriver | |
| parent | ae2d46b87b118669030e8720b166017eeed99231 (diff) | |
further changes for making houdini work
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 35c0832a..82c864d5 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -431,7 +431,17 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.ContractInfer) {
Houdini.Houdini houdini = new Houdini.Houdini(program, true);
- houdini.PerformHoudiniInference();
+ Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment) {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
+ errorCount = outcome.ErrorCount;
+ verified = outcome.Verified;
+ inconclusives = outcome.Inconclusives;
+ timeOuts = outcome.TimeOuts;
+ outOfMemories = 0;
+ return PipelineOutcome.Done;
}
if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
|