Fix4703 (#4705)

Fixes #4703

### Description
Enable the language server to use the options
`disable-nonlinear-arithmetic` and the Z3 executable path, when they are
specified in the project file

### How has this been tested?
A XUnit test has been added for `disable-nonlinear-arithmetic`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/DafnyOptions.cs

@@ -315,7 +315,7 @@ public enum IncludesModes {
     public static string DefaultZ3Version = "4.12.1";
     // Not directly user-configurable, only recorded once we discover it
     public string SolverIdentifier { get; private set; }
-    public Version SolverVersion { get; private set; }
+    public Version SolverVersion { get; set; }
 
     public static readonly ReadOnlyCollection<Plugin> DefaultPlugins =
       new(new[] { SinglePassCompiler.Plugin, InternalDocstringRewritersPluginConfiguration.Plugin });
@@ -1126,7 +1126,7 @@ private void SetZ3Option(string name, string value) {
       }
     }
 
-    private void SetZ3Options(Version z3Version) {
+    public void SetZ3Options(Version z3Version) {
       // Don't allow changing this once set, just in case:
       // a DooFile will record this and will get confused if it changes.
       if ((SolverIdentifier != null && SolverIdentifier != "Z3")

Source/DafnyLanguageServer.Test/ProjectFiles/SolverOptionsTest.cs

@@ -0,0 +1,37 @@
+using System.IO;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Extensions.Logging;
+using Moq;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles;
+
+public class SolverOptionsTest : ClientBasedLanguageServerTest {
+
+  [Fact]
+  public async Task DisableNonLinearArithmeticIsUsed() {
+    var projectFileSource = @"
+[options]
+disable-nonlinear-arithmetic = true".TrimStart();
+
+    var source = @"
+lemma Test(a: real, b: real)
+  requires b != 0.0
+  ensures a / b == 1.0 / b * a
+{}".TrimStart();
+
+    var directory = Path.GetRandomFileName();
+    CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName));
+    var sourceDocument =
+      CreateAndOpenTestDocument(source, Path.Combine(directory, "DisableNonLinearArithmeticIsUsed.dfy"));
+    var diagnostics = await GetLastDiagnostics(sourceDocument);
+    Assert.Single(diagnostics);
+    Assert.Contains("a postcondition", diagnostics.First().Message);
+  }
+
+  public SolverOptionsTest(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) {
+  }
+}

Source/DafnyLanguageServer/Workspace/ProjectManager.cs

@@ -206,6 +206,12 @@ private static DafnyOptions DetermineProjectOptions(DafnyProject projectOptions,
       }
     }
 
+    if (result.SolverIdentifier == "Z3") {
+      result.SolverVersion = null;
+    }
+
+    result.ApplyDefaultOptionsWithoutSettingsDefault();
+
     return result;
   }
 

docs/dev/news/4703.fix

@@ -0,0 +1 @@
+Enable verification options that are configured in a Dafny project file, to be picked up by the Dafny language server