Skip to content

Commit ce0e0c4

Browse files
author
Leonardo
authored
Merge pull request #11754 from ethereum/smt_fix_docs
Add solvers to model checker json docs
2 parents c69c08a + e9e3f12 commit ce0e0c4

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

docs/using-the-compiler.rst

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -410,6 +410,9 @@ Input Description
410410
"engine": "chc",
411411
// Choose whether to output all unproved targets. The default is `false`.
412412
"showUnproved": true,
413+
// Choose which solvers should be used, if available.
414+
// See the Formal Verification section for the solvers description.
415+
"solvers": ["cvc4", "smtlib2", "z3"],
413416
// Choose which targets should be checked: constantCondition,
414417
// underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
415418
// If the option is not given all targets are checked by default.

0 commit comments

Comments
 (0)