diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-08-29 13:32:59 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-08-29 13:32:59 -0700 |
| commit | ebe61ada7635676fafa7d751e2472d69bd46afa8 (patch) | |
| tree | 3bf8919a10ab0d904e002c344845acae4a3a66ed /Source/Provers/SMTLib/Z3.cs | |
| parent | 64b57a073afe03ab57d99c96ef6994b77f786d0e (diff) | |
Add PROVER_PATH prover option (to base options, but currently only used by SMTLib)
Add support for Inspector with latest Z3/SMT2 frontend
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 9b90b12a..847822c1 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -157,6 +157,9 @@ namespace Microsoft.Boogie.SMTLib options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
}
+ if (options.Inspector != null)
+ options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
+
// legacy option handling
if (!CommandLineOptions.Clo.z3AtFlag)
options.MultiTraces = true;
|