OnModel now carries the result of the prover call

1 files changed, 13 insertions, 17 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index e37510a8..22127c5a 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1184,7 +1184,6 @@ namespace VC {
           if (ret == Outcome.Errors && reporter.underapproximationMode)

           {

               // Found a bug

-              reporter.ReportErrors();

               done = 2;

           }

           else if (ret == Outcome.Correct)

@@ -2029,9 +2028,8 @@ namespace VC {
     } // end FCallInliner

 

     public class EmptyErrorHandler : ProverInterface.ErrorHandler {

-      public override void OnModel(IList<string> labels, Model model) {

-

-      }

+        public override void OnModel(IList<string> labels, Model model, ProverInterface.Outcome proverOutcome)

+        { }

     }

 

     public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {

@@ -2214,12 +2212,21 @@ namespace VC {
         return;

       }

 

-      public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {

+      public override void OnResourceExceeded(string message)

+      {

+          //Contract.Requires(message != null);

+      }

+

+      public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {

         if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {

           model.Write(ErrorReporter.ModelWriter);

           ErrorReporter.ModelWriter.Flush();

         }

 

+        // Timeout?

+        if (proverOutcome != ProverInterface.Outcome.Invalid)

+            return;

+

         candidatesToExpand = new List<int>();

         orderedStateIds = new List<Tuple<int, int>>();

         var cex = GenerateTrace(labels, model, 0, mainInfo.impl, mainInfo.mvInfo);

@@ -2227,17 +2234,11 @@ namespace VC {
         if (underapproximationMode && cex != null) {

           //Debug.Assert(candidatesToExpand.All(calls.isSkipped));

           GetModelWithStates(model);

-          this.CexTrace = cex;

+          callback.OnCounterexample(cex, null);

           this.PrintModel(model);

         }

       }

 

-      public void ReportErrors()

-      {

-          if(this.CexTrace != null)

-              callback.OnCounterexample(this.CexTrace, null);

-      }

-

       private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,

                                            int candidateId, Implementation procImpl, ModelViewInfo mvInfo) {

         Contract.Requires(cce.NonNullElements(labels));

@@ -2430,11 +2431,6 @@ namespace VC {
         return cce.NonNull((Absy)l2a[id]);

       }

 

-      public override void OnResourceExceeded(string msg) {

-        //Contract.Requires(msg != null);

-        //resourceExceededMessage = msg;

-      }

-

       public override void OnProverWarning(string msg) {

         //Contract.Requires(msg != null);

         callback.OnWarning(msg);