diff options
| author |  akashlal <unknown> | 2011-02-12 11:30:12 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2011-02-12 11:30:12 +0000 |
| commit | 8926e773af99a75fe1b061a55987fa9f42898f75 (patch) | |
| tree | df78081266ce1e6b3d23f710d2e8d43ab77483d9 /Source/Provers/Z3api | |
| parent | 440d0b46604f1f83a33e861e769e1bee16baf94d (diff) | |
Better support for timeout
Diffstat (limited to 'Source/Provers/Z3api')
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index 97ff41c5..a7ed29eb 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -343,6 +343,12 @@ namespace Microsoft.Boogie.Z3 if (outcome == LBool.False)
break;
+ if (outcome == LBool.Undef && z3Model == null)
+ {
+ // Blame this on timeout
+ return ProverInterface.Outcome.TimeOut;
+ }
+
Debug.Assert(z3Model != null);
LabeledLiterals labels = z3.GetRelevantLabels();
Debug.Assert(labels != null);
|