Dafny sensitive to variable names???

Feb 13, 2013 at 7:29 AM
Hi --- I have some strange behaviour in which Dafny seems to give different results depending on what names are used for functions, even if those functions are not used.

That is (in essence)

function This...
"code not mentioning This or That"

verifies, but

function That...
"code not mentioning This or That"

does not.

I can pass along the code to show this --- but in the meantime I'd appreciate hearing whether this is a known issue.

Feb 13, 2013 at 4:03 PM
No, this is not a known issue. It does on occasion happen that Z3 is fickle, where its internal randomization happens to make some decision a particular way (for example, when picking which case split to do next). If this happens, you would see at the Dafny level see it in some way like that you've described. When Z3 happens to be fickle like that, then reordering the declarations in the Dafny file, adding or removing an otherwise unrelated declarations, or asking Boogie to only verify some particular subset of the procedures can also give the mysterious outcomes. This problem used to happen more frequently than it currently does. I would say that the condition is now rare, but it can occur.

During the Microsoft Hyper-V verification project (a few years ago), the VCC users saw things like this often enough that they would routinely run Z3 with different random seeds. You could try this, passing Z3's /r option down through Dafny:
dafny MyProgram.dfy /z3opt:/r:42
where 42 indicates your chosen random seed. I'm not recommending this as a general consideration when running Dafny (because the fickleness I'm describing does not happen frequently with Dafny and Z3). But trying some different random seeds with your example might show if this is the problem.

A better way to combat problems like when Z3 seems to run out of steam is to use Boogie's options for verification-condition splitting. Do "dafny /help" and look for the options that begin with /vcs. For example, you can do /vcsMaxKeepGoingSplits:2. If you find that verifications take a long time, or that they are fickle like you're seeing, the these are good options to apply. Note that the verification-condition splitting is currently the only way that Boogie takes advantage of parallelism on your processor.

If your "function That..." version never verifies even with the options I've suggested, then it seems time to debug more closely.

Best wishes,