From ba859012a97020a9a65c72d5094da834e1477ef9 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Tue, 16 Nov 2021 15:34:21 +0000 Subject: [PATCH] Add documentation for smtbmc engine --anybase option --- docs/source/reference.rst | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index dc5f336..fd9fc3b 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -231,6 +231,14 @@ the following options: +-----------------+---------------------------------------------------------+ | ``--progress`` | Enable Yosys-SMTBMC timer display. | +-----------------+---------------------------------------------------------+ +| ``--anybase`` | Generate an arbitrary basecase trace in ``prove`` mode, | +| | instead of one derived from the starting conditions. | +| | (This provides a weaker proof that there exists some | +| | basecase for which the assertions hold. | +| | This is powerful when combined with a separate proof | +| | that the assertions hold for ``depth`` cycles after | +| | reset). | ++-----------------+---------------------------------------------------------+ Any SMT2 solver that is compatible with ``yosys-smtbmc`` can be passed as argument to the ``smtbmc`` engine. The solver options are passed to the solver