Improve Z3 detection (#3233)

* Be more explicit about the path of the executable to invoke.
* Identify the version and set different Z3 options accordingly.

Fixes #2370
Enables a fix for #1477
Interacts with #1914 (which may already be fixed)

By submitting this pull request, I confirm that my contribution is made under
the terms of the MIT license.

Source/DafnyCore/DafnyMain.cs

@@ -318,6 +318,19 @@ private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl
  string moduleName,
  Microsoft.Boogie.Program boogieProgram, string programId) {
  var moduleId = (programId ?? "main_program_id") + "_" + moduleName;
+ var z3NotFoundMessage = @"
+Z3 not found. Please either provide a path to the `z3` executable using
+the `--solver-path <path>` option, manually place the `z3` directory
+next to the `dafny` executable you are using (this directory should
+contain `bin/z3` or `bin/z3.exe`), or set the PATH environment variable
+to also include a directory containing the `z3` executable.
+";
+
+ var proverPath = DafnyOptions.O.ProverOptions.Find(o => o.StartsWith("PROVER_PATH="));
+ if (proverPath is null && DafnyOptions.O.Verify) {
+ Console.WriteLine(z3NotFoundMessage);
+ return (PipelineOutcome.FatalError, new PipelineStatistics());
+ }
 
  string bplFilename;
  if (DafnyOptions.O.PrintFile != null) {

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;
@@ -813,8 +814,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;
@@ -1057,35 +1060,85 @@ in such cases in the verifier being faster.
 
  /// <summary>
  /// 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.
  /// </summary>
- 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}'");
+ return null;
  }
- } 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;
+ 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);
+ var z3BinPath = Path.Combine(dafnyBinDir, "z3", "bin", 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) {
+ confirmedProverPath = System.Environment
+ .GetEnvironmentVariable("PATH")?
+ .Split(isUnix ? ':' : ';')
+ .Select(s => Path.Combine(s, z3binName))
+ .FirstOrDefault(File.Exists);
+ }
+
+ if (confirmedProverPath is not null) {
+ ProverOptions.Add($"{pp}{confirmedProverPath}");
+ return GetZ3Version(confirmedProverPath);
+ }
+
+ return null;
+ }
+
+ private static readonly Regex Z3VersionRegex = new Regex(@"Z3 version (?<major>\d+)\.(?<minor>\d+)\.(?<patch>\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.
@@ -1095,7 +1148,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
@@ -1105,10 +1158,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.CompareTo(new Version(4, 8, 5)) <= 0) {
+ // 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");

Source/DafnyDriver.Test/DafnyDriver.Test.csproj

@@ -28,4 +28,10 @@
  <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" />
  </ItemGroup>
 
+ <ItemGroup>
+ <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ </ItemGroup>
+
 </Project>

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) {

Source/TestDafny/TestDafny.csproj

@@ -17,4 +17,10 @@
  <ProjectReference Include="..\XUnitExtensions\XUnitExtensions.csproj" />
  </ItemGroup>
 
+ <ItemGroup>
+ <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3">
+ <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+ </Content>
+ </ItemGroup>
+
 </Project>

Test/cli/badProverPath.dfy

@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %baredafny verify %args --solver-path=doesNotExist "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: Fatal Error: ProverException: Cannot find specified prover:.*
+method m() {
+ assert 1 + 1 == 2;
+}

Test/git-issues/git-issue-401a.dfy.expect

@@ -1 +1 @@
-*** ProverException: Requested prover not found: 'Output/binz/z3'
+Fatal Error: ProverException: Cannot find specified prover: Output/binz/z3