diff options
| author |  Ken McMillan <unknown> | 2013-11-09 15:40:17 -0800 |
|---|---|---|
| committer | Ken McMillan <unknown> | 2013-11-09 15:40:17 -0800 |
| commit | 0172a2eeb76fafd8aaabd34934b41eca15282956 (patch) | |
| tree | 8f0b106fd6c98d980630c20c7f8e101487239cc9 /Source | |
| parent | da2344988055819e33a8737bfdf5e1c6a2bbd0fe (diff) | |
handling timeouts for fixedpoint engines
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 28 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 2 |
3 files changed, 28 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index bc13927f..7418e9e8 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -634,8 +634,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;
@@ -646,6 +659,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;
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index bc9e6992..1d9ff1c4 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -262,6 +262,7 @@ namespace Microsoft.Boogie.SMTLib if (options.TimeLimit > 0)
{
options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());
+ options.AddWeakSmtOption("fixedpoint.TIMEOUT", options.TimeLimit.ToString());
// This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
// options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
}
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 19feabe9..e5bcbc22 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -109,7 +109,7 @@ namespace Microsoft.Boogie program = _program;
gen = ctx;
if(old_checker == null)
- checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);
+ checker = new Checker(this, program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime, null);
else {
checker = old_checker;
checker.Retarget(program,checker.TheoremProver.Context);
|