From e57c9682e6eea7749a0badaafdf731e9784a345e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 13 Sep 2023 13:37:49 -0700 Subject: [PATCH] chore: Mark FuelTrigger wish as now passing (#4546) Evidently, this was fixed by https://github.com/dafny-lang/dafny/pull/4180 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). --- Test/wishlist/FuelTriggers.dfy | 15 +++++++++------ Test/wishlist/FuelTriggers.dfy.expect | 2 +- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/Test/wishlist/FuelTriggers.dfy b/Test/wishlist/FuelTriggers.dfy index d81cce244b8..319b5646909 100755 --- a/Test/wishlist/FuelTriggers.dfy +++ b/Test/wishlist/FuelTriggers.dfy @@ -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) diff --git a/Test/wishlist/FuelTriggers.dfy.expect b/Test/wishlist/FuelTriggers.dfy.expect index ebe2328e072..823a60a105c 100644 --- a/Test/wishlist/FuelTriggers.dfy.expect +++ b/Test/wishlist/FuelTriggers.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 2 verified, 0 errors +Dafny program verifier finished with 1 verified, 0 errors