OnModel now carries the result of the prover call

1 files changed, 3 insertions, 3 deletions

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