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 | |
| parent | 440d0b46604f1f83a33e861e769e1bee16baf94d (diff) | |
Better support for timeout
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 16 |
2 files changed, 22 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);
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 7cb4b3b4..fda8770c 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -833,6 +833,9 @@ namespace VC {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ // Record current time
+ var startTime = DateTime.Now;
+
// Get the checker
Checker checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
@@ -1001,6 +1004,9 @@ namespace VC // Get the checker
Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
+ // Record current time
+ var startTime = DateTime.Now;
+
// Run live variable analysis
if (CommandLineOptions.Clo.LiveVariableAnalysis == 2)
{
@@ -1107,6 +1113,16 @@ namespace VC // case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
while (true)
{
+ // Check timeout
+ if (CommandLineOptions.Clo.ProverKillTime != -1)
+ {
+ if ((DateTime.Now - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
+ {
+ ret = Outcome.TimedOut;
+ break;
+ }
+ }
+
// Note: in the absence of a coverage graph process, the task is always "step"
coverageManager.syncGraph();
var task = coverageManager.getNextTask();
|