Add solvers to model checker json docs

This commit is contained in:
Leo Alt 2021-08-06 17:40:45 +02:00
parent c69c08a26e
commit e9e3f1238f

View File

@ -410,6 +410,9 @@ Input Description
"engine": "chc",
// Choose whether to output all unproved targets. The default is `false`.
"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,
// underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
// If the option is not given all targets are checked by default.