From e9e3f1238f182393f286ba1238eab7da7dccfb3a Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Fri, 6 Aug 2021 17:40:45 +0200
Subject: [PATCH] Add solvers to model checker json docs

---
 docs/using-the-compiler.rst | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst
index cf281b851..afb60acd7 100644
--- a/docs/using-the-compiler.rst
+++ b/docs/using-the-compiler.rst
@@ -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.