Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal that it has reached the recursion bound.

2 files changed, 7 insertions, 5 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index c7761a37..dc13725f 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -360,7 +360,8 @@ namespace VC {
       Errors,

       TimedOut,

       OutOfMemory,

-      Inconclusive

+      Inconclusive,

+      ReachedBound

     }

 

     [ContractInvariantMethod]

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 23b75bbf..8a7edc75 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2198,10 +2198,6 @@ namespace VC {
 	      checker.TheoremProver.Pop();

 	   }

 

-       if (!done)

-       {

-           return Outcome.TimedOut;

-       }

 

        #region Coverage reporter

        if (CommandLineOptions.Clo.CoverageReporterPath == "Console")

@@ -2223,6 +2219,11 @@ namespace VC {
        }

        #endregion

 

+       if (!done)

+       {

+           return Outcome.ReachedBound;

+       }

+

        return ret;

     }