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 #11754 from ethereum/smt_fix_docs

Browse Source 
Add solvers to model checker json docs
This commit is contained in:
Leonardo 2021-08-06 18:50:34 +02:00 committed by GitHub
commit ce0e0c48fb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -410,6 +410,9 @@ Input Description
"engine": "chc", "engine": "chc",
// Choose whether to output all unproved targets. The default is `false`. // Choose whether to output all unproved targets. The default is `false`.
"showUnproved": true, "showUnproved": true,
// Choose which solvers should be used, if available.
// See the Formal Verification section for the solvers description.
"solvers": ["cvc4", "smtlib2", "z3"],
// Choose which targets should be checked: constantCondition, // Choose which targets should be checked: constantCondition,
// underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds. // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
// If the option is not given all targets are checked by default. // If the option is not given all targets are checked by default.