From 9a9991f2131de8e78035581ea2569ba187318ff0 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 7 May 2013 17:40:40 -0700
Subject: Adding fixedpoint engine backend

---
 Source/BoogieDriver/BoogieDriver.cs | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'Source/BoogieDriver')

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);
-- 
cgit v1.2.3