Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CLI: no -arith option in new CLI #5906

Open
bsdinis opened this issue Nov 8, 2024 · 1 comment
Open

CLI: no -arith option in new CLI #5906

bsdinis opened this issue Nov 8, 2024 · 1 comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@bsdinis
Copy link

bsdinis commented Nov 8, 2024

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

@bsdinis bsdinis added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Nov 8, 2024
@keyboardDrummer
Copy link
Member

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

No branches or pull requests

2 participants