summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2013-11-02 19:27:11 +0530
committerGravatar akashlal <unknown>2013-11-02 19:27:11 +0530
commiteb580637a45b8847f404c07274c63859b1d1bcc2 (patch)
tree963a986cfa01121a1516df70bb8984c9c1af6dee /Source/Provers
parentb085703b7432a91000461dd640c47a0df6efdca0 (diff)
ProverInterface: model isn't available on timeout
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index b46e6fea..fe749852 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -855,7 +855,8 @@ namespace Microsoft.Boogie.SMTLib
labels = CalculatePath(handler.StartingProcId());
xlabels = labels;
}
- Model model = GetErrorModel();
+ Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null :
+ GetErrorModel();
handler.OnModel(xlabels, model);
}