Skip to content

Commit e9e3f12

Browse files
author
Leo Alt
committed
Add solvers to model checker json docs
1 parent c69c08a commit e9e3f12

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)