Skip to content

Commit

Permalink
chore: Mark FuelTrigger wish as now passing (dafny-lang#4546)
Browse files Browse the repository at this point in the history
Evidently, this was fixed by
dafny-lang#4180


<small>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).</small>
  • Loading branch information
RustanLeino authored Sep 13, 2023
1 parent 45fa5d0 commit e57c968
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 7 deletions.
15 changes: 9 additions & 6 deletions Test/wishlist/FuelTriggers.dfy
Original file line number Diff line number Diff line change
@@ -1,12 +1,15 @@
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// XFAIL: *

// With the default version of opaque + fuel, the following fails to verify
// because the quantifier in the requires used a trigger that included
// StartFuel_P, while the assert used StartFuelAssert_P. Since P is
// opaque, we can't tell that those fuels are the same, and hence the
// trigger never fires. A wish would be to fix this.
// THIS USED TO BE THE CASE:
//
// With the default version of opaque + fuel, the following fails to verify
// because the quantifier in the requires used a trigger that included
// StartFuel_P, while the assert used StartFuelAssert_P. Since P is
// opaque, we can't tell that those fuels are the same, and hence the
// trigger never fires. A wish would be to fix this.
//
// This has been fixed, so the test assertion is now passing.

ghost predicate {:opaque} P(x:int)

Expand Down
2 changes: 1 addition & 1 deletion Test/wishlist/FuelTriggers.dfy.expect
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Dafny program verifier finished with 2 verified, 0 errors
Dafny program verifier finished with 1 verified, 0 errors

0 comments on commit e57c968

Please sign in to comment.