handling timeouts for fixedpoint engines

1 files changed, 26 insertions, 2 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index bc13927f..7418e9e8 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -634,8 +634,21 @@ namespace Microsoft.Boogie.SMTLib
         {

             

             var resp = Process.GetProverResponse();

-            

-            switch (resp.Name)

+

+            if (proverErrors.Count > 0)

+            {

+                result = Outcome.Undetermined;

+                foreach (var err in proverErrors)

+                {

+                    if (err.Contains("canceled"))

+                    {

+                        result = Outcome.TimeOut;

+                    }

+                }

+            }

+            else if(resp == null)

+                HandleProverError("Prover did not respond");

+            else switch (resp.Name)

             {

                 case "unsat":

                     result = Outcome.Valid;

@@ -646,6 +659,17 @@ namespace Microsoft.Boogie.SMTLib
                 case "unknown":

                     result = Outcome.Invalid;

                     break;

+                case "error":

+                    if (resp.ArgCount > 0 && resp.Arguments[0].Name.Contains("canceled"))

+                    {

+                        result = Outcome.TimeOut;

+                    }

+                    else

+                    {

+                        HandleProverError("Prover error: " + resp.Arguments[0]);

+                        result = Outcome.Undetermined;

+                    }

+                    break;

                 default:

                     HandleProverError("Unexpected prover response: " + resp.ToString());

                     break;