triggering problem on closures

[erniecohen]

Dafny version

4.9.1

Code to produce this issue

type Ord<!T(!new)> = (T,T)->bool
ghost predicate iChain<T(!new)>(o:Ord<T>,c:nat->T) { forall n:nat :: o(c(n),c(n+1)) }
ghost predicate wf<T(!new)>(o:Ord<T>) { forall c:nat->T :: !iChain(o,c) }
type WfO<!T(!new)> = o:Ord<T> | wf(o) witness *
method test<S(!new),T(!new)>(ot:WfO<T>,c:nat->(S,T),j:nat) {
    var c1:nat->T := (i:nat) => c(i+j).1;
    forall c1:nat->T {:trigger iChain(ot,c1)} ensures !iChain(ot,c1) {}
    assert !iChain(ot,c1); // fails quickly
}

Command to run and resulting output

vscode

What happened?

The assert should succeed (e.g. it is an instance of the preceding forall), but fails immediately, so this is presumably a triggering/translation problem. The problem goes away if i+j is replaced by a term not containing j, so presumably the problem is related to the treatment of closures.

What type of operating system are you experiencing the problem on?

Mac