Skip to content

Commit cb4ffbf

Browse files
authored
Fix leftover use of divModWithSlacks in doc
The option `divModWithSlacks` was previously changed to `divModNoSlacks`. However, this was not reflected in the documentation.
1 parent 999a53c commit cb4ffbf

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

docs/using-the-compiler.rst

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -410,12 +410,13 @@ Input Description
410410
"source1.sol": ["contract1"],
411411
"source2.sol": ["contract2", "contract3"]
412412
},
413-
// Choose whether division and modulo operations should be replaced by
414-
// multiplication with slack variables. Default is `true`.
415-
// Using `false` here is recommended if you are using the CHC engine
413+
// Choose how division and modulo operations should be encoded.
414+
// When using `false` they are replaced by multiplication with slack
415+
// variables. This is the default.
416+
// Using `true` here is recommended if you are using the CHC engine
416417
// and not using Spacer as the Horn solver (using Eldarica, for example).
417418
// See the Formal Verification section for a more detailed explanation of this option.
418-
"divModWithSlacks": true,
419+
"divModNoSlacks": false,
419420
// Choose which model checker engine to use: all (default), bmc, chc, none.
420421
"engine": "chc",
421422
// Choose which types of invariants should be reported to the user: contract, reentrancy.

0 commit comments

Comments
 (0)