diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 2606c37..d322d65 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -343,9 +343,9 @@ the following options:
 |                  | warmup the SMT solver).                                 |
 +------------------+---------------------------------------------------------+
 | ``--keep-going`` | In BMC mode, continue after the first failed assertion  |
-|                  | and report further failed assertions. (The ``abc``      |
-|                  | engine also supports ``--keep-going`` with ``pdr``; see |
-|                  | the ``abc`` engine section below.)                      |
+|                  | and report further failed assertions. In prove mode,    |
+|                  | ``--keep-going`` is currently only supported with       |
+|                  | ``abc pdr`` (see the ``abc`` engine section below).     |
 +------------------+---------------------------------------------------------+
 | ``--unroll``,    | Disable/enable unrolling of the SMT problem. The        |
 | ``--nounroll``   | default value depends on the solver being used.         |
@@ -413,8 +413,7 @@ Solver options are passed to the solver as additional command line options.
 ~~~~~~~~~~~~~~
 
 The ``abc`` engine is a front-end for the functionality in Berkeley ABC. It
-currently supports no engine options and supports the following
-solvers:
+supports the following solvers:
 
 +------------+-----------------+---------------------------------+
 |   Solver   |   Modes         |   ABC Command                   |
@@ -430,27 +429,16 @@ Solver options are passed as additional arguments to the ABC command
 implementing the solver.
 
 When using the ``pdr`` solver, the ``abc`` engine supports the following
-engine option:
+engine option (currently the only engine option available for ``abc``):
 
 +------------------+---------------------------------------------------------+
 |   Option         | Description                                             |
 +==================+=========================================================+
 | ``--keep-going`` | Continue after the first proven or failed assertion and |
-|                  | report individual per-property results. When enabled,   |
-|                  | SBY uses the AIGER witness map (``write_aiger -ywmap``) |
-|                  | to track each ``$assert`` cell individually and reports |
-|                  | pass/fail status per property rather than a single      |
-|                  | global result.                                          |
+|                  | report individual per-property results, rather than a   |
+|                  | single global result.                                   |
 +------------------+---------------------------------------------------------+
 
-.. note::
-
-   The ``--keep-going`` option for ``abc pdr`` requires a Yosys version that
-   includes witness-aware AIGER map output (``write_aiger -ywmap`` with
-   assert/assume path tracking) and the ``rename -witness`` pass covering
-   formal property cells.  The default ``prep`` command already runs
-   ``rename -witness``.
-
 Example:
 
 .. code-block:: sby
@@ -458,7 +446,6 @@ Example:
    [engines]
    abc --keep-going pdr
 
-
 ``none`` engine
 ~~~~~~~~~~~~~~~