From 4f9ad03f5d0d6d9a8dbd27adf25b83a3f50d7aa1 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 23 Feb 2011 03:54:37 +0000
Subject: Check for timeout/memoryout

---
 Source/Provers/SMTLib/ProverInterface.cs | 35 ++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index c8c10af9..b0269d2e 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -403,6 +403,7 @@ namespace Microsoft.Boogie.SMTLib
     private Outcome GetResponse()
     {
       var result = Outcome.Undetermined;
+      var wasUnknown = false;
 
       Process.Ping();
 
@@ -416,14 +417,48 @@ namespace Microsoft.Boogie.SMTLib
             result = Outcome.Valid;
             break;
           case "sat":
+            result = Outcome.Invalid;
+            break;
           case "unknown":
             result = Outcome.Invalid;
+            wasUnknown = true;
             break;
           default:
             HandleProverError("Unexpected prover response: " + resp.ToString());
             break;
         }
       }
+
+      if (wasUnknown) {
+        if (options.UseZ3)
+          SendThisVC("(get-info :last-failure)");
+        else
+          SendThisVC("(get-info :reason-unknown)");
+        Process.Ping();
+
+        while (true) {
+          var resp = Process.GetProverResponse();
+          if (resp == null || Process.IsPong(resp))
+            break;
+
+          if (resp.ArgCount == 1 && (resp.Name == ":reason-unknown" || resp.Name == ":last-failure")) {
+            switch (resp[0].Name) {
+              case "memout":
+                result = Outcome.OutOfMemory;
+                break;
+              case "timeout":
+                result = Outcome.TimeOut;
+                break;
+              default:
+                break;
+            }
+          } else {
+            HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString());
+          }
+        }
+
+      }
+
       return result;
     }
 
-- 
cgit v1.2.3