Skip to content

Commit

Permalink
Bump Boogie to v3.0.12 (#5105)
Browse files Browse the repository at this point in the history
### Description

Bump Boogie to v3.0.12. This adds features useful for debugging and
experimentation that we don't expect most people to use.

### How has this been tested?

The existing test suite covers the relevant functionality.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.
  • Loading branch information
atomb authored Feb 20, 2024
1 parent e49dec6 commit 67daee7
Show file tree
Hide file tree
Showing 4 changed files with 11 additions and 9 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/DafnyCore.csproj
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
<PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
<PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
<PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
<PackageReference Include="Boogie.ExecutionEngine" Version="3.0.11" />
<PackageReference Include="Boogie.ExecutionEngine" Version="3.0.12" />
<PackageReference Include="Tomlyn" Version="0.16.2" />
</ItemGroup>

Expand Down
2 changes: 1 addition & 1 deletion customBoogie.patch
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644
<PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
<PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
<PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
- <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.11" />
- <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.12" />
+ <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
+ <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
+ <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />
Expand Down
14 changes: 8 additions & 6 deletions docs/DafnyRef/Options.txt
Original file line number Diff line number Diff line change
Expand Up @@ -619,12 +619,14 @@ Usage: dafny [ option ... ] [ filename ... ]
the SMT theory of arrays. This option allows the use of axioms instead.
/reflectAdd In the VC, generate an auxiliary symbol, elsewhere defined
to be +, instead of +.
/prune
Turn on pruning. Pruning will remove any top-level Boogie declarations
that are not accessible by the implementation that is about to be verified.
Without pruning, due to the unstable nature of SMT solvers,
a change to any part of a Boogie program has the potential
to affect the verification of any other part of the program.
/prune:<n>
0 - Turn off pruning.
1 - Turn on pruning (default). Pruning will remove any top-level
Boogie declarations that are not accessible by the implementation
that is about to be verified. Without pruning, due to the unstable
nature of SMT solvers, a change to any part of a Boogie program
has the potential to affect the verification of any other part of
the program.

Only use this if your program contains uses clauses
where required, otherwise pruning will break your program.
Expand Down
2 changes: 1 addition & 1 deletion dotnet-tools.json
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
]
},
"boogie": {
"version": "3.0.9",
"version": "3.0.12",
"commands": [
"boogie"
]
Expand Down

0 comments on commit 67daee7

Please sign in to comment.