diff options
| author |  Ken McMillan <kenmcmil@microsoft.com> | 2013-05-07 17:40:40 -0700 |
|---|---|---|
| committer | Ken McMillan <kenmcmil@microsoft.com> | 2013-05-07 17:40:40 -0700 |
| commit | 9a9991f2131de8e78035581ea2569ba187318ff0 (patch) | |
| tree | 5f2c0d4e85c9713f4d6663d26b49f67b5fbb27f0 /Source/BoogieDriver | |
| parent | 77aeb920de2c3cd22a1296700305539f28f6761c (diff) | |
Adding fixedpoint engine backend
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);
|