Dafny Encounters internal translation error for nested quantifier expressions when a subtitute is required

[arminvakil]

Dafny version

4.5.0.0

Code to produce this issue

ghost predicate bar(x:int, y:int)    

ghost predicate foo(s:seq<int>)
{
    forall i: int | 0 <= i < |s| - 1 :: 
        var current: int, next: int := s[i], s[i + 1]; 
        && bar(current, next)
        && exists m | m in s :: true
}

Command to run and resulting output

dafny error.dfy
error.dfy(6,49): Error: undeclared identifier: _t#0#0
error.dfy(6,49): Error: undeclared identifier: _t#0#0
error.dfy(6,49): Error: undeclared identifier: _t#0#0
error.dfy(6,49): Error: undeclared identifier: _t#0#0
error.dfy(6,49): Error: undeclared identifier: _t#0#0
error.dfy(6,49): Error: undeclared identifier: _t#0#0
6 name resolution errors detected in /tmp/error__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/tmp/error__module.bpl(3233,99): Error: undeclared identifier: _t#0#0
/tmp/error__module.bpl(3239,101): Error: undeclared identifier: _t#0#0
/tmp/error__module.bpl(3252,109): Error: undeclared identifier: _t#0#0
/tmp/error__module.bpl(3258,111): Error: undeclared identifier: _t#0#0
/tmp/error__module.bpl(3354,101): Error: undeclared identifier: _t#0#0
/tmp/error__module.bpl(3361,99): Error: undeclared identifier: _t#0#0
6 name resolution errors detected in /tmp/error__module.bpl

What happened?

In the forallExpr, dafny chooses s[i] as selected trigger, and it next tries to substitute s[i+1] with _t#0 when calling PostCyclicityResolve function (

dafny/Source/DafnyCore/Resolver/ModuleResolver.cs

Line 179 in 480758f

rewriter.PostCyclicityResolve(module, Reporter);

) for TriggerGeneratingRewriter.

Some comments regarding this approach is mentioned here:

dafny/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs

Line 73 in 480758f

// rewrite quantifier to avoid matching loops

This eventually calls to the Substitute function in ExprSubstituter class and instead of adding this variable to the forallExpr, it is added to the nested existsExpr and causes an error in boogie because of undeclared identifier in the forallExpr body.

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

Linux