search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.92k stars 262 forks source link

Differences in Verification Depending on CLI style? #3837

Open DavePearce opened 1 year ago

DavePearce commented 1 year ago

Dafny version

3.13.0

Code to produce this issue

dafny /randomSeedIterations:5 /vcsLoad:1 /functionSyntax:4 src/test/dafny/proofs/FM-paper.dfy

Command to run and resulting output

dafny verify --boogie "/randomSeedIterations:5 /vcsLoad:1" --function-syntax:4 src/test/dafny/proofs/FM-paper.dfy

What happened?

The outcome of these two commands very consistent. The first always verifies without trouble. The second always fails. The only visible difference is that, in the latter, I'm using the new CLI style. Unfortunaterly, I don't really know how to narrow the test code itself down as its part of a larger code base (which is open source, so we can see it).

My feeling is that there are some differences in the command-line given to Boogie, depending on which of the commands above is run. Is it possible to see the command-line it uses?

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

Linux

keyboardDrummer commented 1 year ago

My feeling is that there are some differences in the command-line given to Boogie

Sounds likely yes

Is it possible to see the command-line it uses?

I don't think there is: https://github.com/boogie-org/boogie/issues/475