cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #12741 from david-k/develop

Browse Source 
[Doc] Fix leftover use of divModWithSlacks
This commit is contained in:
Leo 2022-03-07 10:12:47 +01:00 committed by GitHub
commit 7c91dd05a7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
docs/using-the-compiler.rst
View File

@ -410,12 +410,13 @@ Input Description
"source1.sol": ["contract1"],
"source2.sol": ["contract2", "contract3"]
},
// Choose whether division and modulo operations should be replaced by
// multiplication with slack variables. Default is `true`.
// Using `false` here is recommended if you are using the CHC engine
// Choose how division and modulo operations should be encoded.
// When using `false` they are replaced by multiplication with slack
// variables. This is the default.
// Using `true` here is recommended if you are using the CHC engine
// and not using Spacer as the Horn solver (using Eldarica, for example).
// See the Formal Verification section for a more detailed explanation of this option.
"divModWithSlacks": true,
"divModNoSlacks": false,
// Choose which model checker engine to use: all (default), bmc, chc, none.
"engine": "chc",
// Choose which types of invariants should be reported to the user: contract, reentrancy.