Wrong conjunct mentioned in "related location" under a quantifier

[wilcoxjay]

Consider this Dafny program.

predicate P1(a: int)
predicate P2(a: int)

predicate Q(s: seq<int>) {
  forall i | 0 <= i < |s| ::
    (P1(s[i]) || false) && (P2(s[i]) || false)  // Line 6
}

method M(s: seq<int>)
  requires forall i | 0 <= i < |s| :: P1(s[i])
  // requires forall i | 0 <= i < |s| :: P2(s[i])
  ensures Q(s)
{}

The method M has an error because it is missing the commented-out precondition about P2. But Dafny reports the following error misleading messages:

issue2211.dfy(13,0): Error: A postcondition might not hold on this return path.
issue2211.dfy(12,10): Related location: This is the postcondition that might not hold.
issue2211.dfy(5,2): Related location
issue2211.dfy(6,14): Related location

Dafny program verifier finished with 2 verified, 1 error

The last "Related location" points to the first conjunct (the 14th character on the 6th line), but in fact the first conjunct is true and the problem is with the second conjunct.

On the other hand, Dafny behaves correctly when not under a quantifier, as in this example:

predicate P1(a: int)
predicate P2(a: int)

predicate Q(s: seq<int>) {
  |s| > 0 && P1(s[0]) && P2(s[0])
}

method M(s: seq<int>)
  requires |s| > 0
  requires P1(s[0])
  ensures Q(s)
{}

which generates

issue2211.dfy(12,0): Error: A postcondition might not hold on this return path.
issue2211.dfy(11,10): Related location: This is the postcondition that might not hold.
issue2211.dfy(5,25): Related location

Dafny program verifier finished with 2 verified, 1 error

The 25th character of the 5th line correctly points to the third conjunct, because the first two are true.

This is a relatively serious usability issue, and I feel like it is a regression that used to work?

I reproduced this error on the main branch.

[MikaelMayer]

Thanks for reporting this issue !
Did it behave differently with a previous version of Dafny?

[wilcoxjay]

Not sure. Like I said, I have a feeling that this used to work, because it is somewhat fundamental to my workflow when I use Dafny, and I would have noticed it before if it was broken. But these days I only use Dafny to answer stack overflow questions, so it's hard for me to know exactly when it broke.

I suppose I will try to find some time to do a git bisect.

[MikaelMayer]

I confirm that the behavior was the same in Dafny 3.1.0

[MikaelMayer]

And you don't need || false, the error is the same.

[MikaelMayer]

If you split the forall, I confirm that the error reporting works as expected.

(forall i | 0 <= i < |s| ::
    P1(s[i])) 
  && (forall i | 0 <= i < |s| ::  // Related location 3
    P2(s[i]))  // Related location 4

What you demonstrate is clearly an error in error reporting.

[wilcoxjay]

And you don't need || false, the error is the same.

Right. I should have mentioned that I put the || false in there solely to disambiguate between the error location being at the beginning of the line (which you might think means "the whole line") versus inside the first conjunct.

[wilcoxjay]

Ok, I used Clément's new script to try all previous releases, and it turns out I was wrong. This behavior goes back to at least v1.9.9.

[wilcoxjay]

Slightly simpler example

predicate P1(a: int)
predicate P2(a: int)

method M()
  requires forall i :: P1(i)
  //requires forall i :: P2(i)
  ensures forall i ::
      (P1(i) || false)  // related location
    && (P2(i) || false)
{}