Added "extra recursion bound" to FixedpointVC to support Corral.

2 files changed, 6 insertions, 2 deletions

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);