diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-10-21 17:13:17 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-10-21 17:13:17 -0700 |
| commit | 8297862e06741335a86a60a6ea52645d46f9be96 (patch) | |
| tree | 11d25031a8b670f27be88499d6c748a00d592f68 /Source/Provers/SMTLib/Z3.cs | |
| parent | 4b1eae86e95f1599999a0d4ce01efd56ffcb3e99 (diff) | |
Don't pass /T: option to Z3 - it kills Z3 prematurely when there are multiple queries
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 847822c1..f9e90427 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -154,7 +154,8 @@ namespace Microsoft.Boogie.SMTLib if (options.TimeLimit > 0) {
options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
- options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
+ // 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);
}
if (options.Inspector != null)
|