summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
authorGravatar Michal Moskal <michal@moskal.me>2011-10-21 17:24:48 -0700
committerGravatar Michal Moskal <michal@moskal.me>2011-10-21 17:24:48 -0700
commit7759b2d59c5df01df981a2ca846b86ba98b5ada9 (patch)
tree978da0897b0ec0dea9052e5df9068e39160b9f51 /Source/Provers/SMTLib/ProverInterface.cs
parent8297862e06741335a86a60a6ea52645d46f9be96 (diff)
Sync timeout messages with Z3 prover interface
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 5e9aef4d..e70f2bae 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -525,9 +525,11 @@ namespace Microsoft.Boogie.SMTLib
if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") {
switch (resp[0].Name) {
case "memout":
+ currentErrorHandler.OnResourceExceeded("memory");
result = Outcome.OutOfMemory;
break;
case "timeout":
+ currentErrorHandler.OnResourceExceeded("timeout");
result = Outcome.TimeOut;
break;
default: