Skip to content

Conversation

@RustanLeino
Copy link
Collaborator

Previously, every use of an assume statement with an {:axiom} annotation gave rise to the following warning:

assume statement has no {:axiom} annotation

This wording causes most new Dafny users to decorate their assume statements with {:axiom}, which defeats the purpose of the warning and misuses the {:axiom} annotation. The idea behind the warning is to alert the user that here is an assume statement that should eventually be removed (this happens if the assume is added temporarily during verification debugging) or confirmed to be a permanent axiom. The idea behind the {:axiom} annotation is to confirm that this use of the assume is really intended to be in the code permanently, so no warning should be generated.

This PR changes the warning message to

program contains an assume statement (to suppress this warning, annotate the statement with {:axiom})

which is more to the point.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@RustanLeino RustanLeino marked this pull request as ready for review December 10, 2025 19:49
@RustanLeino RustanLeino enabled auto-merge (squash) December 10, 2025 19:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant