Complete this form and hit the "Save Changes" button!
4 ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// In one version of opaque + fuel, the following failed 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
predicate {:opaque} P(x:int)
method test(y:int)
requires forall x :: P(x);
{
assert P(y);
}
