Assertion too true to fail?

May 7, 2014 at 6:52 AM
Hi --- I have a longish program (which I'll email privately) that contains a "helpful assertion" that boils down to
assert seq[0..|seq|] == seq;
for a sequence (of integers). Every now and then (not every time) Dafny 1.8.2 flags this as an assertion failure. The "every so often" we have discussed before (randomness inherent in Z3); but maybe it's strange that this assertion should -ever- fail. Is this fact hard to verify?

Thus I'd be glad of any suggestions as to why Dafny could find such an assertion difficult. (This particular program is proving a real pain to verify.)

Thanks!
Coordinator
May 8, 2014 at 1:11 AM
I tried out your program. It's really random. It seems to verify about half the time. As far as I can tell, the nondeterminism comes from Boogie, probably from the order in which it gets procedures to be verified off the work queue. This causes the VCs to be presented to Z3 in different orders, and for some of these, Z3 gives up the ghost (probably because it goes down some unfruitful path in its proof exploration and then hits some limit).

So, I don't think it's the too-true-to-fail assertion that is at fault. Rather, that's where Z3 ends up when it runs out of its limits. I will send some email (and will CC you) to see if we can get better resolution on this.

Rustan
May 8, 2014 at 3:12 AM
Dear Rustan,

Thanks for looking into this one.

For the record, the commented-out method calls, and assert/assume groups after them, were my attempt to isolate the randomness: I found it easier to fiddle around when things were in-line. Ideally (and where I started from), the methods were actually called, and the assert/assumes were commented out.. But usually Dafny would just loop unless I put in extra helpful assertions.

And strangely those helpful assertions were often just one of the loop invariants, placed at the end of the do-od alternative. I took that to be influencing the order in which things were verified; but I have little intuition about how to get further.

Looking forward to learning more!