diff options
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index c12ba47d..1ee9bab6 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -743,10 +743,18 @@ 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);
+ }
+ else if (CommandLineOptions.Clo.FixedPointEngine != null)
+ {
+ vcgen = new FixedpointVC(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);
}
} catch (ProverException e) {
ErrorWriteLine("Fatal Error: ProverException: {0}", e);
|