In what order are isolated assertions verified?

[hmijail]

What change in documentation do you suggest?

In the JSON log of dafny measure-complexity --isolated-assertions, are vcResults assigned a vcNum according to their verification order? For example, is vcNum 1 verified before vcNum 2?

Asking because I have a log that lists the vcNums of the vcResults of a verificationResult out of order. E.g., I'm seeing a vcResult list with vcNums [4,1,3,2] in the JSON. So I wonder if they are being verified in JSON order or in vcNum order. This is important because, IIUC, if e.g. vcNum 3 fails verification, then subsequent verifications are unreliable.

When those example vcNums are sorted as [1,2,3,4], their line:col follow the order one encounters when reading the source code. This is the order that I intuitively (naively?) expected for verification. However some languages change the order of evaluation of things; so I wonder how this works during Dafny's verification.

Issue #5805 also made me think of this.

[hmijail]

I noticed that with --cores=1, the JSON order seems to be the vcNum order. So I guess that solves one source of order variation.

Still remains the question of whether verification of vcNum x+1 logically follows vcNum x.