OnModel now carries the result of the prover call

6 files changed, 21 insertions, 25 deletions

diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs
index a85adbe1..8d89bae3 100644
--- a/Source/Doomed/DoomErrorHandler.cs
+++ b/Source/Doomed/DoomErrorHandler.cs
@@ -62,7 +62,7 @@ namespace VC
             }

         }

 

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

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

         {

             // TODO: it would be better to check which reachability variables are actually set to one!

             List<Block> traceNodes = new List<Block>();

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 57ef660d..8b038554 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -4602,7 +4602,7 @@ namespace Microsoft.Boogie.Houdini {
             model = null;

         }

 

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

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

         {

             Debug.Assert(model != null);

             if(CommandLineOptions.Clo.PrintErrorModel >= 1) model.Write(Console.Out);

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index b5d9bc3d..fd7c1bda 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -1255,7 +1255,7 @@ namespace Microsoft.Boogie.SMTLib
             }

               Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null :

                   GetErrorModel();

-            handler.OnModel(xlabels, model);

+            handler.OnModel(xlabels, model, result);

           }

 

           if (labels == null || !labels.Any() || errorsLeft == 0) break;

@@ -1431,14 +1431,14 @@ namespace Microsoft.Boogie.SMTLib
         }

       }

 

+      

       if (wasUnknown) {

         SendThisVC("(get-info :reason-unknown)");

         Process.Ping();

-

         while (true) {

           var resp = Process.GetProverResponse();

           if (resp == null || Process.IsPong(resp))

-            break;

+              break;

 

           if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") {

             switch (resp[0].Name) {

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index a77bfba5..9fc301da 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -461,7 +461,7 @@ namespace Microsoft.Boogie {
           return 0;

       }

 

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

+      public virtual void OnModel(IList<string> labels, Model model, Outcome proverOutcome) {

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

       }

 

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);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 53868e1d..bfff8f0e 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1881,7 +1881,7 @@ namespace VC {
         this.program = program;

       }

 

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

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

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

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

           if (VC.ConditionGeneration.errorModelList != null)

@@ -1970,7 +1970,7 @@ namespace VC {
         Contract.Requires(program != null);

       }

 

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

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

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

         // We ignore the error model here for enhanced error message purposes.

         // It is only printed to the command line.