diff options
| author |  MichalMoskal <unknown> | 2011-02-23 03:54:37 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-23 03:54:37 +0000 |
| commit | 4f9ad03f5d0d6d9a8dbd27adf25b83a3f50d7aa1 (patch) | |
| tree | 211c84a7560a1ab91ab07f6d687ff21f9d83aa17 /Source/Provers | |
| parent | 8e1c309880067303b9fa847184338db682dc78de (diff) | |
Check for timeout/memoryout
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 35 |
1 files changed, 35 insertions, 0 deletions
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;
}
|