diff options
Diffstat (limited to 'Source/BoogieDriver/BoogieDriver.cs')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 88d8bdaa..35c0832a 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -429,6 +429,11 @@ namespace Microsoft.Boogie { // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ if (CommandLineOptions.Clo.ContractInfer) {
+ Houdini.Houdini houdini = new Houdini.Houdini(program, true);
+ houdini.PerformHoudiniInference();
+ }
+
if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
}
|