From 6a2badc34adb07adbd572feeeee12b8f27ce0d1f Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 24 Feb 2023 18:17:17 -0800 Subject: [PATCH] Revert "Update build to use both Z3 4.8.5 and 4.12.1 (#3622)" (#3636) This reverts commit a9a65ebce4e40bfe19be3fd8e200a3b6c9e52a7a. 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). --- .github/workflows/doc-tests.yml | 7 +- .../workflows/integration-tests-reusable.yml | 19 ++-- .github/workflows/release-downloads-nuget.yml | 45 ++++----- .github/workflows/release-downloads.yml | 9 +- .github/workflows/xunit-tests.yml | 16 +-- Makefile | 26 ++--- Source/DafnyCore/DafnyOptions.cs | 11 +-- .../Various/ResourceUsageTest.cs | 4 +- .../DafnyLanguageServer.cs | 10 +- Source/IntegrationTests/LitTests.cs | 4 +- Test/git-issues/BoundedInts.dfy | 37 +++++++ Test/git-issues/Wrappers.dfy | 98 +++++++++++++++++++ Test/git-issues/git-issue-1514.dfy | 2 +- Test/git-issues/git-issue-1514b.dfy | 2 +- Test/git-issues/git-issue-1514c.dfy | 2 +- Test/git-issues/git-issue-2927.dfy | 2 +- Test/git-issues/git-issue1495.dfy | 2 +- Test/lit.site.cfg | 2 +- 18 files changed, 212 insertions(+), 86 deletions(-) create mode 100644 Test/git-issues/BoundedInts.dfy create mode 100644 Test/git-issues/Wrappers.dfy diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml index 405f2a6d6c7..1c441a8bd1c 100644 --- 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 index 5c4347e3c57..0096528c3df 100644 --- 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 index 7bb360d904e..29c9533e640 100644 --- 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 index 7db050d75e1..7e62dde0519 100644 --- 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 index 9ad98938e74..c7359d8e50a 100644 --- 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 index 59211fc4d0c..2b7e24db4be 100644 --- 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 index d868ac306d3..0cf4b34b9f5 100644 --- 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 DefaultPlugins = new(new[] { SinglePassCompiler.Plugin }); private IList cliPluginCache; public IList Plugins => cliPluginCache ??= ComputePlugins(); @@ -1098,14 +1096,12 @@ 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; @@ -1113,12 +1109,11 @@ private Version SetZ3ExecutablePath() { } // 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 index 2ce112bdbae..918f4dab459 100644 --- 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); } -} +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index 368a6534d24..62aa59cf5b2 100644 --- 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 index 2ba71393807..5da7298ef72 100644 --- 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 AddExtraArgs(IEnumerable args, IEnumerable 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 new file mode 100644 index 00000000000..bbae0a6abef --- /dev/null +++ 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 + +} diff --git a/Test/git-issues/Wrappers.dfy b/Test/git-issues/Wrappers.dfy new file mode 100644 index 00000000000..56f267a4628 --- /dev/null +++ b/Test/git-issues/Wrappers.dfy @@ -0,0 +1,98 @@ +// RUN: %diff "%s" "%s" +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module {:options "-functionSyntax:4"} Wrappers { + + datatype Option<+T> = None | Some(value: T) { + function ToResult(): Result { + match this + case Some(v) => Success(v) + case None() => Failure("Option is None") + } + + function UnwrapOr(default: T): T { + match this + case Some(v) => v + case None() => default + } + + predicate IsFailure() { + None? + } + + function PropagateFailure(): Option + requires None? + { + None + } + + function Extract(): T + requires Some? + { + value + } + } + + datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) { + function ToOption(): Option + { + match this + case Success(s) => Some(s) + case Failure(e) => None() + } + + function UnwrapOr(default: T): T + { + match this + case Success(s) => s + case Failure(e) => default + } + + predicate IsFailure() { + Failure? + } + + function PropagateFailure(): Result + requires Failure? + { + Failure(this.error) + } + + function MapFailure(reWrap: R -> NewR): Result + { + match this + case Success(s) => Success(s) + case Failure(e) => Failure(reWrap(e)) + } + + function Extract(): T + requires Success? + { + value + } + } + + datatype Outcome = Pass | Fail(error: E) + { + predicate IsFailure() { + Fail? + } + // Note: PropagateFailure returns a Result, not an Outcome. + function PropagateFailure(): Result + requires Fail? + { + Failure(this.error) + } + // Note: no Extract method + } + + // A helper function to ensure a requirement is true at runtime + // :- Need(5 == |mySet|, "The set MUST have 5 elements.") + function Need(condition: bool, error: E): (result: Outcome) + { + if condition then Pass else Fail(error) + } +} diff --git a/Test/git-issues/git-issue-1514.dfy b/Test/git-issues/git-issue-1514.dfy index fe106472092..07a1a6a7dd2 100644 --- a/Test/git-issues/git-issue-1514.dfy +++ b/Test/git-issues/git-issue-1514.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -include "../libraries/src/Wrappers.dfy" +include "Wrappers.dfy" import opened Wrappers trait Foo { diff --git a/Test/git-issues/git-issue-1514b.dfy b/Test/git-issues/git-issue-1514b.dfy index 7044b070517..1d8cd122d28 100644 --- a/Test/git-issues/git-issue-1514b.dfy +++ b/Test/git-issues/git-issue-1514b.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -include "../libraries/src/Wrappers.dfy" +include "Wrappers.dfy" import opened Wrappers trait Foo { diff --git a/Test/git-issues/git-issue-1514c.dfy b/Test/git-issues/git-issue-1514c.dfy index 26c7b34d637..d9df7d108c1 100644 --- a/Test/git-issues/git-issue-1514c.dfy +++ b/Test/git-issues/git-issue-1514c.dfy @@ -3,7 +3,7 @@ // RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t" // RUN: %diff "%s.expect" "%t" -include "../libraries/src/Wrappers.dfy" +include "Wrappers.dfy" import opened Wrappers method id(r: T) returns (r2: T) { diff --git a/Test/git-issues/git-issue-2927.dfy b/Test/git-issues/git-issue-2927.dfy index fd8d1cbb4a1..e9432c30767 100644 --- a/Test/git-issues/git-issue-2927.dfy +++ b/Test/git-issues/git-issue-2927.dfy @@ -1,7 +1,7 @@ // RUN: %exits-with 0 %dafny /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -include "../libraries/src/BoundedInts.dfy" +include "BoundedInts.dfy" module {:options "-functionSyntax:4"} DafnyNaCl { diff --git a/Test/git-issues/git-issue1495.dfy b/Test/git-issues/git-issue1495.dfy index cfed32b199a..5d56da718ab 100644 --- a/Test/git-issues/git-issue1495.dfy +++ b/Test/git-issues/git-issue1495.dfy @@ -1,6 +1,6 @@ // RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -include "../libraries/src/Wrappers.dfy" +include "Wrappers.dfy" import opened Wrappers datatype Bar = Bar(i: string) diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index 3deaeea2500..4c320ba6e74 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -215,7 +215,7 @@ solverRoots = os.pathsep.join( print(solverRoots) solverPath = \ - lit.util.which("z3-4.8.5", solverRoots) or \ + lit.util.which("z3", solverRoots) or \ lit.util.which("cvc4", solverRoots) if not solverPath: