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

1 files changed, 5 insertions, 4 deletions

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;

     }