search

dafny-lang / dafny

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

CLI: no -arith option in new CLI #5906

Open bsdinis opened 2 weeks ago

bsdinis commented 2 weeks ago

Dafny version

4.9.0+25fa1000744d8d8a9a6a84c0712149daeda6f67e

Code to produce this issue

module Empty { }

Command to run and resulting output

$ dafny verify Empty.dfy
Dafny program verifier finished with 0 verified, 0 errors
$ dafny verify Empty.dfy -arith:5
CLI: Error: command-line argument '-arith:5' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).
$ dafny verify Example.i.dfy -noCheating:1
CLI: Error: command-line argument '-noCheating:1' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).

What happened?

According to the documentation -arith:<n> and -noCheating:<n> are valid (albeit legacy) CLI options.

I am attempting to move a tool from the old CLI to the tool and cannot find an alternative to these legacy CLI options (and it doesn't even appear to exist when running dafny verify --help).

Any help would be much appreciated!

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

Linux

keyboardDrummer commented 1 week ago

What value for /arith are you using? There's no replacement for /arith in the new CLI. There is --disable-nonlinear-arithmetic though and the standard library contains many lemma's that relate to nonlinear arithmetic.

noCheating also does not exist in the new CLI. However, Dafny now produces a warning for any assume statement, and warnings are treated much more strictly in the new CLI. Unless --allow-warnings is used, any warning will prevent Dafny from running or generating executable code.