Merge FixpointVC changes with mainline

2 files changed, 6 insertions, 2 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 8cee2675..da8624e9 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -494,7 +494,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 4b4e970e..7dbf6b05 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -1521,6 +1521,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)

             {

@@ -1532,12 +1533,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);