From 60a3fea864bb86f8f5c325743707709b3016e3f0 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 13 Mar 2024 16:11:11 -0700 Subject: [PATCH] Bump Boogie dependency to v3.1.3 (#5190) ### Description Bump Boogie dependency to v3.1.3 This most importantly includes https://github.com/boogie-org/boogie/pull/859 ### How has this been tested? Existing tests should be sufficient. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --- Source/DafnyCore/DafnyCore.csproj | 2 +- customBoogie.patch | 2 +- docs/DafnyRef/Options.txt | 5 +++++ dotnet-tools.json | 2 +- 4 files changed, 8 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index a371664ecfe..2dfb8efd4c4 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/customBoogie.patch b/customBoogie.patch index be7b342b7c5..4bb29486f56 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + + diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index e63f4242bb3..b5d88209010 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -646,6 +646,11 @@ Usage: dafny [ option ... ] [ filename ... ] report. This generalizes and replaces the previous (undocumented) `/printNecessaryAssertions` option. + /keepQuantifier + If pool-based quantifier instantiation creates instances of a quantifier + then keep the quantifier along with the instances. By default, the quantifier + is dropped if any instances are created. + ---- Verification-condition splitting -------------------------------------- /vcsMaxCost: diff --git a/dotnet-tools.json b/dotnet-tools.json index 977e4a10a0e..c263d70700e 100644 --- a/dotnet-tools.json +++ b/dotnet-tools.json @@ -9,7 +9,7 @@ ] }, "boogie": { - "version": "3.1.2", + "version": "3.1.3", "commands": [ "boogie" ]