clean up in stratified inlining

1 files changed, 16 insertions, 0 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index cc81be5b..5eda8263 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -472,6 +472,22 @@ namespace VC {
       ReachedBound

     }

 

+    public static Outcome ProverInterfaceOutcomeToConditionGenerationOutcome(ProverInterface.Outcome outcome) {

+      switch (outcome) {

+        case ProverInterface.Outcome.Invalid:

+          return Outcome.Errors;

+        case ProverInterface.Outcome.OutOfMemory:

+          return Outcome.OutOfMemory;

+        case ProverInterface.Outcome.TimeOut:

+          return Outcome.TimedOut;

+        case ProverInterface.Outcome.Undetermined:

+          return Outcome.Inconclusive;

+        case ProverInterface.Outcome.Valid:

+          return Outcome.Correct;

+      }

+      return Outcome.Inconclusive;  // unreachable but the stupid compiler does not understand

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(checkers));