1 files changed, 17 insertions, 0 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 2c202022..ed3d1afc 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -261,6 +261,7 @@ namespace Microsoft.Boogie.Houdini {
       this.callGraph = BuildCallGraph();
       this.continueAtError = continueAtError;
       this.houdiniConstants = CollectExistentialConstants();
+      Inline();
       this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
       this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
 
@@ -277,6 +278,22 @@ namespace Microsoft.Boogie.Houdini {
       this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
     }
 
+    private void Inline() {
+      if (CommandLineOptions.Clo.InlineDepth < 0)
+        return;
+      foreach (Implementation impl in callGraph.Nodes) {
+        impl.OriginalBlocks = impl.Blocks;
+        impl.OriginalLocVars = impl.LocVars;
+      }
+      foreach (Implementation impl in callGraph.Nodes) {
+        Inliner.ProcessImplementationForHoudini(program, impl);
+      }
+      foreach (Implementation impl in callGraph.Nodes) {
+        impl.OriginalBlocks = null;
+        impl.OriginalLocVars = null;
+      }
+    }
+
     private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
       Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();
       foreach (Declaration decl in program.TopLevelDeclarations) {