Skip to content

Commit 60a3fea

Browse files
authored
Bump Boogie dependency to v3.1.3 (#5190)
### Description Bump Boogie dependency to v3.1.3 This most importantly includes boogie-org/boogie#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.
1 parent b144df2 commit 60a3fea

File tree

4 files changed

+8
-3
lines changed

4 files changed

+8
-3
lines changed

Source/DafnyCore/DafnyCore.csproj

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@
3434
<PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
3535
<PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
3636
<PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
37-
<PackageReference Include="Boogie.ExecutionEngine" Version="3.1.2" />
37+
<PackageReference Include="Boogie.ExecutionEngine" Version="3.1.3" />
3838
<PackageReference Include="Tomlyn" Version="0.16.2" />
3939
</ItemGroup>
4040

customBoogie.patch

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644
6161
<PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
6262
<PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
6363
<PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
64-
- <PackageReference Include="Boogie.ExecutionEngine" Version="3.1.2" />
64+
- <PackageReference Include="Boogie.ExecutionEngine" Version="3.1.3" />
6565
+ <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
6666
+ <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
6767
+ <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />

docs/DafnyRef/Options.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -646,6 +646,11 @@ Usage: dafny [ option ... ] [ filename ... ]
646646
report. This generalizes and replaces the previous
647647
(undocumented) `/printNecessaryAssertions` option.
648648

649+
/keepQuantifier
650+
If pool-based quantifier instantiation creates instances of a quantifier
651+
then keep the quantifier along with the instances. By default, the quantifier
652+
is dropped if any instances are created.
653+
649654
---- Verification-condition splitting --------------------------------------
650655

651656
/vcsMaxCost:<f>

dotnet-tools.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
]
1010
},
1111
"boogie": {
12-
"version": "3.1.2",
12+
"version": "3.1.3",
1313
"commands": [
1414
"boogie"
1515
]

0 commit comments

Comments
 (0)