Skip to content

Commit

Permalink
added correct syntax for smt_groundQuantifiers after Jeffery Sholtz c… (
Browse files Browse the repository at this point in the history
#303)

* added correct syntax for smt_groundQuantifiers after Jeffery Sholtz complained

* removing = sign from more prover args
  • Loading branch information
urikirsh authored Oct 2, 2024
1 parent 8eecd7b commit 0aae4fb
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions docs/prover/cli/options.md
Original file line number Diff line number Diff line change
Expand Up @@ -985,7 +985,7 @@ Prover. `--prover_args` receives a string containing Prover-specific options, a
set by `--smt_timeout` therefore cannot appear in `--prover_args`). `--prover_args` value must be quoted

(-optimisticreturnsize)=
#### `--prover_args '-optimisticReturnsize=true'`
#### `--prover_args '-optimisticReturnsize true'`

This option determines whether {ref}`havoc summaries <havoc-summary>` assume
that the called method returns the correct number of return values.
Expand All @@ -999,7 +999,7 @@ the expected size matching the methods in the scene.
Otherwise, `RETURNSIZE` will remain non-deterministic.

(-superoptimisticreturnsize)=
#### `--prover_args '-superOptimisticReturnsize=true'`
#### `--prover_args '-superOptimisticReturnsize true'`

This option determines whether {ref}`havoc summaries <havoc-summary>` assume
that the called method returns the correct number of return values.
Expand All @@ -1020,7 +1020,7 @@ effectively restricting a `mathint` to a `uint256`. We currently do not have a
setting or encoding that models precisely both bitwise operations and `mathint`.

(-smt_groundquantifiers)=
#### `--prover_args -smt_groundQuantifiers=false`
#### `--prover_args '-smt_groundQuantifiers false'`

This option disables quantifier grounding. See {ref}`grounding` for more
information.
Expand Down

0 comments on commit 0aae4fb

Please sign in to comment.