diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index d99c2e1..2606c37 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -343,7 +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.                   |
+|                  | and report further failed assertions. (The ``abc``      |
+|                  | engine also supports ``--keep-going`` with ``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.         |
@@ -427,6 +429,35 @@ solvers:
 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:
+
++------------------+---------------------------------------------------------+
+|   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.                                          |
++------------------+---------------------------------------------------------+
+
+.. 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
+
+   [engines]
+   abc --keep-going pdr
+
 
 ``none`` engine
 ~~~~~~~~~~~~~~~