summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2010-11-23 07:06:26 +0000
committerGravatar akashlal <unknown>2010-11-23 07:06:26 +0000
commit6de6a788ea56b36b802e7b44fe67199c3b7b7e53 (patch)
tree472a1e8d9bb73dab52e724475d8389991dff571a /Source/BoogieDriver
parentfd9227b188714c56402024a42b5d07e7d73d8fbc (diff)
Refactoring: pulled out all code for stratified inlining to a new file.
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 0fc67e15..98c1b9da 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -479,6 +479,8 @@ namespace Microsoft.Boogie {
try {
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ } else if(CommandLineOptions.Clo.StratifiedInlining > 0) {
+ vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
} else {
vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
}