Revert "Update build to use both Z3 4.8.5 and 4.12.1 (#3622)" (#3636)

This reverts commit a9a65eb. <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>
dafny-lang · Feb 25, 2023 · 6a2badc · 6a2badc
1 parent 3a8666e
commit 6a2badc
Show file tree

Hide file tree

Showing 18 changed files with 212 additions and 86 deletions.
diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml
@@ -35,10 +35,9 @@ jobs:
     - name: Load Z3
       run: |
         sudo apt-get install -qq libarchive-tools
-        mkdir -p dafny/Binaries/z3/bin
-        wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17/z3-4.8.5-ubuntu-20.04-bin.zip | bsdtar -xf -
-        mv z3-* dafny/Binaries/z3/bin/
-        chmod +x dafny/Binaries/z3/bin/z3-*
+        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
+        chmod +x dafny/Binaries/z3/bin/z3
     - name: Build Dafny
       run: dotnet build dafny/Source/Dafny.sln
     - name: Check OnlineTutorial examples

diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml
@@ -98,8 +98,10 @@ jobs:
       uses: actions/checkout@v3
       with:
         path: dafny
-        submodules: true
-    - run: rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override
+        submodules: false # Until the libraries work again
+#    - name: Clean up libraries for testing
+#      run: |
+#        rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override
     - name: Create release
       if: inputs.all_platforms
       run: |
@@ -115,13 +117,12 @@ jobs:
       if: "!inputs.all_platforms"
       run: |
         sudo apt-get install -qq libarchive-tools
-        mkdir -p dafny/Binaries/z3/bin
-        wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17/z3-4.8.5-ubuntu-20.04-bin.zip | bsdtar -xf -
-        mv z3-4.8.5 dafny/Binaries/z3/bin/
-        chmod +x dafny/Binaries/z3/bin/z3-4.8.5
+        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
+        chmod +x dafny/Binaries/z3/bin/z3
         mkdir -p unzippedRelease/dafny/z3/bin
-        ln dafny/Binaries/z3/bin/z3-4.8.5 unzippedRelease/dafny/z3/bin/z3-4.8.5
-    - name: Run integration tests
+        ln dafny/Binaries/z3/bin/z3 unzippedRelease/dafny/z3/bin/z3
+    - name: Run integration tests (Windows)
       if: runner.os == 'Windows'
       env:
         XUNIT_SHARD: ${{ matrix.shard }}
@@ -130,7 +131,7 @@ jobs:
       run: |
         cmd /c mklink D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3 D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3.exe
         dotnet test --logger trx dafny/Source/IntegrationTests/IntegrationTests.csproj
-    - name: Run integration tests
+    - name: Run integration tests (non-Windows)
       if: runner.os != 'Windows'
       env:
         XUNIT_SHARD: ${{ matrix.shard }}

diff --git a/.github/workflows/release-downloads-nuget.yml b/.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/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17
+  z3BaseUri: https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5
 
 jobs:
   test-dafny-cli-tool:
@@ -28,16 +28,20 @@ jobs:
       fail-fast: false
       matrix:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-22.04, ubuntu-20.04, macos-11, windows-2019 ]
+        os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
         include:
-        - os:  'ubuntu-22.04'
-          osn: 'ubuntu\-22.04'
+        - 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
         - os:  'macos-latest'
-          osn: 'osx-11'
+          osn: 'osx-.*'
+          z3: z3-4.8.5-x64-osx-10.14.2
         - os:  'windows-2019'
           osn: 'win'
+          z3: z3-4.8.5-x64-win
 
     steps:
     - name: OS
@@ -54,20 +58,14 @@ jobs:
     - name: Load Z3
       shell: pwsh
       run: |
-        Invoke-WebRequest ${{env.z3BaseUri}}/z3-4.8.5-${{matrix.os}}-bin.zip -OutFile z3-4.8.5.zip
-        Invoke-WebRequest ${{env.z3BaseUri}}/z3-4.12.1-${{matrix.os}}-bin.zip -OutFile z3-4.12.1.zip
-        Expand-Archive z3-4.8.5.zip .
-        Expand-Archive z3-4.12.1.zip .
-        Remove-Item z3-4.8.5.zip
-        Remove-Item z3-4.12.1.zip
-    - name: Set up Z3
+        Invoke-WebRequest ${{env.z3BaseUri}}/${{matrix.z3}}.zip -OutFile z3.zip
+        Expand-Archive z3.zip .
+        Remove-Item z3.zip
+    - name: Set Z3 permissions
       run: |
         mkdir bin
-        mv z3-* bin/
-    - name: Make Z3 executable (non-Windows)
-      run: |
-        chmod +x bin/z3-*
-      if: runner.os != 'Windows'
+        mv ${{matrix.z3}}/bin/z3* bin/
+        chmod +x bin/z3*
     - name: Set Path
       if: runner.os != 'Windows'
       run: echo "${PWD}/bin" >> $GITHUB_PATH
@@ -85,8 +83,7 @@ jobs:
     ## Check that dafny and z3 run and that a simple program verifies or fails
     - name: Versions
       run: |
-        z3-4.8.5 -version
-        z3-4.12.1 -version
+        z3 -version
         dafny -version
     - name: Fatch latest release version string
       id: dafny
@@ -142,14 +139,18 @@ jobs:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
         os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
         include:
-        - os:  'ubuntu-22.04'
-          osn: 'ubuntu\-22.04'
+        - os:  'ubuntu-latest'
+          osn: 'ubuntu\-20.04'
+          z3: z3-4.8.5-x64-ubuntu-16.04
         - os:  'ubuntu-20.04'
           osn: 'ubuntu\-20.04'
-        - os:  'macos-11'
+          z3: z3-4.8.5-x64-ubuntu-16.04
+        - os:  'macos-latest'
           osn: 'osx-.*'
+          z3: z3-4.8.5-x64-osx-10.14.2
         - os:  'windows-2019'
           osn: 'win'
+          z3: z3-4.8.5-x64-win
 
     steps:
     ## Verify that the dependencies of the libraries we publish (e.g. DafnyLanguageServer)

diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml
@@ -16,11 +16,11 @@ jobs:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
         os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ]
         include:
-        - os:  'ubuntu-22.04'
-          osn: 'ubuntu\-22.04'
+        - os:  'ubuntu-latest'
+          osn: 'ubuntu\-20.04'
         - os:  'ubuntu-20.04'
           osn: 'ubuntu\-20.04'
-        - os:  'macos-11'
+        - os:  'macos-latest'
           osn: 'x64-osx-.*'
         - os:  'windows-2019'
           osn: 'win'
@@ -62,8 +62,7 @@ jobs:
     ## Check that dafny and z3 run and that a simple program verifies or fails
     - name: Versions
       run: |
-        dafny/z3/bin/z3-4.8.5 -version
-        dafny/z3/bin/z3-4.12.1 -version
+        dafny/z3/bin/z3 -version
         dafny/dafny -version
     - name: Check
       run: dafny/dafny /compileVerbose:0 /compile:0 a.dfy

diff --git a/.github/workflows/xunit-tests.yml b/.github/workflows/xunit-tests.yml
@@ -31,21 +31,24 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - os: macos-11
+          - os: macos-latest
             suffix: osx
+            z3: z3-4.8.5-x64-osx-10.14.2
             chmod: true
             coverage: false
           - os: windows-2019
             suffix: win
+            z3: z3-4.8.5-x64-win
             chmod: false
             coverage: false
           - os: ubuntu-20.04
             suffix: ubuntu-20.04
+            z3: z3-4.8.5-x64-ubuntu-16.04
             chmod: true
             coverage: true
     env:
       solutionPath: Source/Dafny.sln
-      z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17
+      z3BaseUri: https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5
       Logging__LogLevel__Microsoft: Debug
     steps:
     - uses: actions/checkout@v3
@@ -60,17 +63,14 @@ jobs:
     - name: Load Z3
       shell: pwsh
       run: |
-        Invoke-WebRequest ${{env.z3BaseUri}}/z3-4.8.5-${{matrix.os}}-bin.zip -OutFile z3.zip
+        Invoke-WebRequest ${{env.z3BaseUri}}/${{matrix.z3}}.zip -OutFile z3.zip
         Expand-Archive z3.zip .
         Remove-Item z3.zip
-    - name: Move Z3
-      run: |
-        mkdir -p Binaries/z3/bin
-        mv z3-* Binaries/z3/bin/
+        Copy-Item ${{matrix.z3}} Binaries/z3 -Recurse
     - name: Set Z3 Permissions
       if: ${{matrix.chmod}}
       run: |
-        chmod +x Binaries/z3/bin/z3*
+        chmod +x Binaries/z3/bin/z3
     - name: Build
       run: dotnet build -warnaserror --no-restore ${{env.solutionPath}}
     - name: Run DafnyLanguageServer Tests

diff --git a/Makefile b/Makefile
@@ -25,26 +25,16 @@ refman-release:
 	make -C ${DIR}/docs/DafnyRef release
 
 z3-mac:
-	mkdir -p ${DIR}Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17/z3-4.12.1-macos-11-bin.zip
-	unzip z3-4.12.1-macos-11-bin.zip
-	rm z3-4.12.1-macos-11-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17/z3-4.8.5-macos-11-bin.zip
-	unzip z3-4.8.5-macos-11-bin.zip
-	rm z3-4.8.5-macos-11-bin.zip
-	mv z3-* ${DIR}/Binaries/z3/bin/
-	chmod +x ${DIR}/Binaries/z3/bin/z3-*
+	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
+	rm z3-4.8.5-x64-osx-10.14.2.zip
 
 z3-ubuntu:
-	mkdir -p ${DIR}Binaries/z3/bin
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17/z3-4.12.1-ubuntu-20.04-bin.zip
-	unzip z3-4.12.1-ubuntu-20.04-bin.zip
-	rm z3-4.12.1-ubuntu-20.04-bin.zip
-	wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-02-17/z3-4.8.5-ubuntu-20.04-bin.zip
-	unzip z3-4.8.5-ubuntu-20.04-bin.zip
-	rm z3-4.8.5-ubuntu-20.04-bin.zip
-	mv z3-* ${DIR}/Binaries/z3/bin/
-	chmod +x ${DIR}/Binaries/z3/bin/z3-*
+	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
+	rm z3-4.8.5-x64-ubuntu-16.04.zip
 
 format:
 	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
@@ -324,8 +324,6 @@ public enum IncludesModes {
 
     public bool AuditProgram = false;
 
-    public static string DefaultZ3Version = "4.8.5";
-
     public static readonly ReadOnlyCollection<Plugin> DefaultPlugins = new(new[] { SinglePassCompiler.Plugin });
     private IList<Plugin> cliPluginCache;
     public IList<Plugin> Plugins => cliPluginCache ??= ComputePlugins();
@@ -1098,27 +1096,24 @@ private Version SetZ3ExecutablePath() {
 
       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 z3LocalBinName = isUnix
-          ? $"z3-{DefaultZ3Version}"
-          : $"z3-{DefaultZ3Version}.exe";
-        var z3BinPath = Path.Combine(dafnyBinDir, "z3", "bin", z3LocalBinName);
+        var z3BinPath = Path.Combine(dafnyBinDir, "z3", "bin", z3binName);
 
         if (File.Exists(z3BinPath)) {
           confirmedProverPath = z3BinPath;
         }
       }
 
       // Finally, try looking in the system PATH variable.
-      var z3GlobalBinName = isUnix ? "z3" : "z3.exe";
       if (confirmedProverPath is null) {
         confirmedProverPath = System.Environment
           .GetEnvironmentVariable("PATH")?
           .Split(isUnix ? ':' : ';')
-          .Select(s => Path.Combine(s, z3GlobalBinName))
+          .Select(s => Path.Combine(s, z3binName))
           .FirstOrDefault(File.Exists);
       }
 

diff --git a/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs b/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs
@@ -17,7 +17,7 @@ method Foo()
 {
     assert false;
 }";
-    string solverProcessName = $"z3-{DafnyOptions.DefaultZ3Version}";
+    const string solverProcessName = "z3";
     var processes1 = Process.GetProcessesByName(solverProcessName);
     var documentItem = CreateTestDocument(source);
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
@@ -30,4 +30,4 @@ method Foo()
     var processes3 = Process.GetProcessesByName(solverProcessName);
     Assert.AreEqual(processes2.Length, processes3.Length);
   }
-}
+}
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
@@ -71,11 +71,17 @@ private static void PublishSolverPath(ILanguageServer server) {
 
     private static void HandleZ3Version(ITelemetryPublisher telemetryPublisher, SMTLibSolverOptions proverOptions) {
       var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
-      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
+      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)) {
         return;
       }
 
-      telemetryPublisher.PublishZ3Version($"Z3 version {z3Version}");
+      telemetryPublisher.PublishZ3Version("Z3 version {major}.{minor}.{patch}");
 
       var toReplace = "O:model_compress=false";
       var i = DafnyOptions.O.ProverOptions.IndexOf(toReplace);

diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs
@@ -33,7 +33,7 @@ public class LitTests {
       "/proverOpt:O:smt.qi.eager_threshold=100",
       "/proverOpt:O:smt.delay_units=true",
       "/proverOpt:O:smt.arith.solver=2",
-      "/proverOpt:PROVER_PATH:" + RepositoryRoot + $"../unzippedRelease/dafny/z3/bin/z3-{DafnyOptions.DefaultZ3Version}"
+      "/proverOpt:PROVER_PATH:" + RepositoryRoot + "../unzippedRelease/dafny/z3/bin/z3"
     };
 
     private static readonly LitTestConfiguration Config;
@@ -58,7 +58,7 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         { "%diff", "diff" },
         { "%trargs", "--use-basename-for-filename --cores:2 --verification-time-limit:300" },
         { "%binaryDir", "." },
-        { "%z3", Path.Join("z3", "bin", $"z3-{DafnyOptions.DefaultZ3Version}") },
+        { "%z3", Path.Join("z3", "bin", "z3") },
         { "%repositoryRoot", RepositoryRoot.Replace(@"\", "/") },
       };
 

diff --git a/Test/git-issues/BoundedInts.dfy b/Test/git-issues/BoundedInts.dfy
@@ -0,0 +1,37 @@
+// RUN: %diff "%s" "%s"
+module {:options "-functionSyntax:4"} BoundedInts {
+  const TWO_TO_THE_0:   int := 1
+
+  const TWO_TO_THE_1:   int := 2
+  const TWO_TO_THE_2:   int := 4
+  const TWO_TO_THE_4:   int := 16
+  const TWO_TO_THE_5:   int := 32
+  const TWO_TO_THE_8:   int := 0x100
+  const TWO_TO_THE_16:  int := 0x10000
+  const TWO_TO_THE_24:  int := 0x1000000
+  const TWO_TO_THE_32:  int := 0x1_00000000
+  const TWO_TO_THE_40:  int := 0x100_00000000
+  const TWO_TO_THE_48:  int := 0x10000_00000000
+  const TWO_TO_THE_56:  int := 0x1000000_00000000
+  const TWO_TO_THE_64:  int := 0x1_00000000_00000000
+  const TWO_TO_THE_128: int := 0x1_00000000_00000000_00000000_00000000
+  const TWO_TO_THE_256: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000
+  const TWO_TO_THE_512: int :=
+    0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000;
+
+  newtype uint8 = x: int  | 0 <= x < TWO_TO_THE_8
+  newtype uint16 = x: int | 0 <= x < TWO_TO_THE_16
+  newtype uint32 = x: int | 0 <= x < TWO_TO_THE_32
+  newtype uint64 = x: int | 0 <= x < TWO_TO_THE_64
+
+  newtype int8 = x: int   | -0x80 <= x < 0x80
+  newtype int16 = x: int  | -0x8000 <= x < 0x8000
+  newtype int32 = x: int  | -0x8000_0000 <= x < 0x8000_0000
+  newtype int64 = x: int  | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000
+
+  newtype nat8 = x: int   | 0 <= x < 0x80
+  newtype nat16 = x: int  | 0 <= x < 0x8000
+  newtype nat32 = x: int  | 0 <= x < 0x8000_0000
+  newtype nat64 = x: int  | 0 <= x < 0x8000_0000_0000_0000
+
+}