summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
authorGravatar Ken McMillan <unknown>2013-11-09 15:45:09 -0800
committerGravatar Ken McMillan <unknown>2013-11-09 15:45:09 -0800
commit334d29e2e34647caa2defd9cd0d329e1e9f0dfd3 (patch)
tree31d51078b4fc87fe7b4d3fc361d61084e84b613b /Source/Provers/SMTLib/ProverInterface.cs
parent762424bf2a12558fd5a1eacbc056ebff3193b318 (diff)
parent0172a2eeb76fafd8aaabd34934b41eca15282956 (diff)
Merge duality changes to mainline
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs28
1 files changed, 26 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index fe749852..c5c867d9 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -673,8 +673,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;
@@ -685,6 +698,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;