diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 189be194719..46fcb91eb61 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -7,6 +7,7 @@
using System.CommandLine;
using System.CommandLine.Binding;
using System.CommandLine.Parsing;
+using System.Diagnostics;
using System.Linq;
using System.Diagnostics.Contracts;
using System.IO;
@@ -816,8 +817,10 @@ public void ApplyDefaultOptionsWithoutSettingsDefault() {
// expand macros in filenames, now that LogPrefix is fully determined
- SetZ3ExecutablePath();
- SetZ3Options();
+ if (!ProverOptions.Any(x => x.StartsWith("SOLVER=") && !x.EndsWith("=z3"))) {
+ var z3Version = SetZ3ExecutablePath();
+ SetZ3Options(z3Version);
+ }
// Ask Boogie to perform abstract interpretation
UseAbstractInterpretation = true;
@@ -1060,35 +1063,89 @@ in such cases in the verifier being faster.
///
/// Dafny releases come with their own copy of Z3, to save users the trouble of having to install extra dependencies.
- /// For this to work, Dafny looks for Z3 at the location where it is put by our release script (i.e., z3/bin/z3[.exe]).
- /// If Z3 is not found there, Dafny relies on Boogie to locate Z3 (which also supports setting a path explicitly on the command line).
- /// Developers (and people getting Dafny from source) need to install an appropriate version of Z3 themselves.
+ /// For this to work, Dafny first tries any prover path explicitly provided by the user, then looks for for the copy
+ /// distributed with Dafny, and finally looks in any directory in the system PATH environment variable.
///
- private void SetZ3ExecutablePath() {
+ private Version SetZ3ExecutablePath() {
+ string confirmedProverPath = null;
+
+ // Try an explicitly provided prover path, if there is one.
var pp = "PROVER_PATH=";
var proverPathOption = ProverOptions.Find(o => o.StartsWith(pp));
if (proverPathOption != null) {
var proverPath = proverPathOption.Substring(pp.Length);
// Boogie will perform the ultimate test to see if "proverPath" is real--it will attempt to run it.
// However, by at least checking if the file exists, we can produce a better error message in common scenarios.
+ // Unfortunately, there doesn't seem to be a portable way of checking whether it's executable.
if (!File.Exists(proverPath)) {
throw new Bpl.ProverException($"Requested prover not found: '{proverPath}'");
}
- } else {
- var platform = (int)System.Environment.OSVersion.Platform;
- var isUnix = platform == 4 || platform == 6 || platform == 128;
+ confirmedProverPath = proverPath;
+ }
- var z3binName = isUnix ? "z3" : "z3.exe";
+ var platform = System.Environment.OSVersion.Platform;
+ var isUnix = platform == PlatformID.Unix || platform == PlatformID.MacOSX || (int)platform == 128;
+ var z3binName = isUnix ? "z3" : "z3.exe";
+
+ // Next, try looking in a directory relative to Dafny itself.
+ if (confirmedProverPath is null) {
var dafnyBinDir = Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location);
var z3BinDir = Path.Combine(dafnyBinDir, "z3", "bin");
var z3BinPath = Path.Combine(z3BinDir, z3binName);
if (File.Exists(z3BinPath)) {
- // Let's use z3BinPath
- ProverOptions.Add($"{pp}{z3BinPath}");
+ confirmedProverPath = z3BinPath;
}
}
+
+ // Finally, try looking in the system PATH variable.
+ if (confirmedProverPath is null) {
+ var z3InPATH = System.Environment
+ .GetEnvironmentVariable("PATH")!
+ .Split(isUnix ? ':' : ';')
+ .Select(s => Path.Combine(s, z3binName))
+ .FirstOrDefault(File.Exists);
+ if (z3InPATH is not null) {
+ confirmedProverPath = z3InPATH;
+ }
+ }
+
+ if (confirmedProverPath is not null) {
+ ProverOptions.Add($"{pp}{confirmedProverPath}");
+ return GetZ3Version(confirmedProverPath);
+ }
+
+ throw new Bpl.ProverException("Z3 not found in Dafny distribution or PATH environment variable.");
+ }
+
+ private static readonly Regex Z3VersionRegex = new Regex(@"Z3 version (?\d+)\.(?\d+)\.(?\d+)");
+
+ [CanBeNull]
+ public static Version GetZ3Version(string proverPath) {
+ var z3Process = new ProcessStartInfo(proverPath, "-version") {
+ CreateNoWindow = true,
+ RedirectStandardError = true,
+ RedirectStandardOutput = true,
+ RedirectStandardInput = true
+ };
+ var run = Process.Start(z3Process);
+ if (run == null) {
+ return null;
+ }
+
+ var actualOutput = run.StandardOutput.ReadToEnd();
+ run.WaitForExit();
+ var versionMatch = Z3VersionRegex.Match(actualOutput);
+ if (!versionMatch.Success) {
+ // Might be another solver.
+ return null;
+ }
+
+ var major = int.Parse(versionMatch.Groups["major"].Value);
+ var minor = int.Parse(versionMatch.Groups["minor"].Value);
+ var patch = int.Parse(versionMatch.Groups["patch"].Value);
+ return new Version(major, minor, patch);
}
// Set a Z3 option, but only if it is not overwriting an existing option.
@@ -1098,7 +1155,7 @@ private void SetZ3Option(string name, string value) {
}
}
- private void SetZ3Options() {
+ private void SetZ3Options(Version z3Version) {
// Boogie sets the following Z3 options by default:
// smt.mbqi = false
// model.compact = false
@@ -1108,10 +1165,14 @@ private void SetZ3Options() {
// Boogie also used to set the following options, but does not anymore.
SetZ3Option("auto_config", "false");
SetZ3Option("type_check", "true");
- SetZ3Option("smt.case_split", "3"); // TODO: try removing
SetZ3Option("smt.qi.eager_threshold", "100"); // TODO: try lowering
SetZ3Option("smt.delay_units", "true");
- SetZ3Option("smt.arith.solver", "2");
+
+ if (z3Version is not null && z3Version.Major == 4 && z3Version.Minor == 8 && z3Version.Build == 5) {
+ // These options tend to help with Z3 4.8.5 but hurt with newer versions of Z3.
+ SetZ3Option("smt.case_split", "3");
+ SetZ3Option("smt.arith.solver", "2");
+ }
if (DisableNLarith || 3 <= ArithMode) {
SetZ3Option("smt.arith.nl", "false");
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
index 5debac48260..62aa59cf5b2 100644
--- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs
+++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
@@ -70,33 +70,19 @@ private static void PublishSolverPath(ILanguageServer server) {
}
private static void HandleZ3Version(ITelemetryPublisher telemetryPublisher, SMTLibSolverOptions proverOptions) {
- var z3Process = new ProcessStartInfo(proverOptions.ProverPath, "-version") {
- CreateNoWindow = true,
- RedirectStandardError = true,
- RedirectStandardOutput = true,
- RedirectStandardInput = true
- };
- var run = Process.Start(z3Process);
- if (run == null) {
- return;
- }
-
- var actualOutput = run.StandardOutput.ReadToEnd();
- run.WaitForExit();
- var versionMatch = Z3VersionRegex.Match(actualOutput);
- if (!versionMatch.Success) {
- // Might be another solver.
+ var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
+ if (z3Version is null) {
return;
}
-
- telemetryPublisher.PublishZ3Version(versionMatch.Value);
- var major = int.Parse(versionMatch.Groups["major"].Value);
- var minor = int.Parse(versionMatch.Groups["minor"].Value);
- var patch = int.Parse(versionMatch.Groups["patch"].Value);
+ var major = z3Version.Major;
+ var minor = z3Version.Minor;
+ var patch = z3Version.Build;
if (major <= 4 && (major < 4 || minor <= 8) && (minor < 8 || patch <= 6)) {
return;
}
+ telemetryPublisher.PublishZ3Version("Z3 version {major}.{minor}.{patch}");
+
var toReplace = "O:model_compress=false";
var i = DafnyOptions.O.ProverOptions.IndexOf(toReplace);
if (i == -1) {