From 1cca1f3efef31b9eee79bb26a5032da2620a8365 Mon Sep 17 00:00:00 2001
From: Ken McMillan <unknown>
Date: Wed, 8 Oct 2014 13:36:42 -0700
Subject: Added "extra recursion bound" to FixedpointVC to support Corral.

---
 Source/VCGeneration/Check.cs        | 2 +-
 Source/VCGeneration/FixedpointVC.cs | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 9fc301da..cf822bb0 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -498,7 +498,7 @@ namespace Microsoft.Boogie {
     
     public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler,
                                      out RPFP.Node cex,
-                                     Dictionary<int, Dictionary<string, string>> varSubst)
+                                     Dictionary<int, Dictionary<string, string>> varSubst, Dictionary<string,int> extra_bound = null)
     {
         throw new System.NotImplementedException();
     }
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 9f39e46c..974765fc 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -1568,6 +1568,7 @@ namespace Microsoft.Boogie
             RPFP.Node cex;
             varSubst = new Dictionary<int,Dictionary<string,string>>();
 
+#if false
             int origRecursionBound = CommandLineOptions.Clo.RecursionBound;
             if (CommandLineOptions.Clo.RecursionBound > 0 && extraRecBound != null)
             {
@@ -1579,12 +1580,15 @@ namespace Microsoft.Boogie
                 }
                 CommandLineOptions.Clo.RecursionBound += maxExtra;
             }
+#endif
             
             ProverInterface.Outcome outcome =
-                 checker.TheoremProver.CheckRPFP("name", rpfp, handler, out cex, varSubst);
+                 checker.TheoremProver.CheckRPFP("name", rpfp, handler, out cex, varSubst, extraRecBound);
             cexroot = cex;
 
+#if false
             CommandLineOptions.Clo.RecursionBound = origRecursionBound;
+#endif
           
             Console.WriteLine("solve: {0}s", (DateTime.Now - start).TotalSeconds);
             
-- 
cgit v1.2.3