diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-06-30 18:46:42 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-06-30 18:46:42 -0700 |
| commit | dfbb0d7413d68c094c6fc243ea57a3b720bdc048 (patch) | |
| tree | 68082b2cf61c1dfebe75488b948855151fba2cad /Source | |
| parent | 7a145e0fdc83fe13a7e9819e9c13e19e1b785fae (diff) | |
Add /T: option to Z3 to kill it if it exceeds soft timeout by more than 1s
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 54742802..da9e8faa 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -157,8 +157,10 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("WARNING", "false");
}
- if (options.TimeLimit > 0)
+ if (options.TimeLimit > 0) {
options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
+ options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
+ }
// legacy option handling
if (!CommandLineOptions.Clo.z3AtFlag)
|