Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index a4635f49..a0005263 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -617,6 +617,11 @@ namespace Microsoft.Boogie {
             default:

               Contract.Assert(false);  // unexpected outcome

               throw new cce.UnreachableException();

+            case VCGen.Outcome.ReachedBound:

+              Inform(String.Format("{0}verified", timeIndication));

+              Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));

+              verified++;

+              break;

             case VCGen.Outcome.Correct:

               if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

                 Inform(String.Format("{0}credible", timeIndication));