diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 62c79f60b..0c49e84b8 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -930,12 +930,9 @@ struct AigerBackend : public Backend {
 		log("        make indexes zero based, enable using map files with smt solvers.\n");
 		log("\n");
 		log("    -ywmap <filename>\n");
-		log("        write a map file for conversion to and from yosys witness traces.\n");
-		log("        The generated JSON map includes \"asserts\" and \"assumes\" arrays\n");
-		log("        containing the hierarchical witness paths of the corresponding\n");
-		log("        $assert and $assume cells. This enables downstream tools to map\n");
-		log("        AIGER bad-state properties and invariant constraints back to\n");
-		log("        individual formal properties by name.\n");
+		log("        write a map file for conversion to and from yosys witness traces,\n");
+		log("        also allows for mapping AIGER bad-state properties and invariant\n");
+		log("        constraints back to individual formal properties by name.\n");
 		log("\n");
 		log("    -I, -O, -B, -L\n");
 		log("        If the design contains no input/output/assert/flip-flop then create one\n");
diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst
index da9193a6f..b418f6aff 100644
--- a/docs/source/using_yosys/more_scripting/model_checking.rst
+++ b/docs/source/using_yosys/more_scripting/model_checking.rst
@@ -121,29 +121,29 @@ Result with fixed :file:`axis_master.v`:
 Witness framework and per-property tracking
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-When using AIGER-based formal verification flows (such as the ``abc`` engine in
-SymbiYosys), Yosys provides infrastructure for tracking individual formal
+When using AIGER-based formal verification flows (such as the `abc` engine in
+SBY), Yosys provides infrastructure for tracking individual formal
 properties through the verification pipeline.
 
-The ``rename -witness`` pass (run automatically by ``prep``) assigns public
+The `rename -witness` pass (run automatically by `prep`) assigns public
 names to all cells that participate in the witness framework:
 
-- Witness signal cells: ``$anyconst``, ``$anyseq``, ``$anyinit``,
-  ``$allconst``, ``$allseq``
-- Formal property cells: ``$assert``, ``$assume``, ``$cover``, ``$live``,
-  ``$fair``, ``$check``
+- Witness signal cells: `$anyconst`, `$anyseq`, `$anyinit`,
+  `$allconst`, `$allseq`
+- Formal property cells: `$assert`, `$assume`, `$cover`, `$live`,
+  `$fair`, `$check`
 
 These public names allow downstream tools to refer to individual properties by
 their hierarchical path rather than by anonymous internal identifiers.
 
-The ``write_aiger -ywmap`` option generates a JSON map file that includes, among
+The `write_aiger -ywmap` option generates a JSON map file that includes, among
 other things, ``"asserts"`` and ``"assumes"`` arrays.  Each entry contains the
-hierarchical witness path of the corresponding ``$assert`` or ``$assume`` cell.
-This lets tools such as SymbiYosys map AIGER bad-state properties and invariant
+hierarchical witness path of the corresponding `$assert` or `$assume` cell.
+This lets tools such as SBY map AIGER bad-state properties and invariant
 constraints back to individual formal properties, enabling features like
-per-property pass/fail reporting (e.g. ``abc pdr`` with ``--keep-going`` mode).
+per-property pass/fail reporting (e.g. `abc pdr` with ``--keep-going`` mode).
 
-The ``write_smt2`` backend similarly uses the public witness names when emitting
+The `write_smt2` backend similarly uses the public witness names when emitting
 ``yosys-smt2-assert`` and ``yosys-smt2-assume`` comments.  Cells whose
 ``hdlname`` attribute contains the ``_witness_`` marker are treated as having
 private names for comment purposes, keeping solver output clean.
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index f87396743..836dfe5b1 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -262,15 +262,10 @@ struct RenamePass : public Pass {
 		log("\n");
 		log("    rename -witness\n");
 		log("\n");
-		log("Assigns auto-generated names to all $any*/$all* output wires and containing\n");
-		log("cells that do not have a public name. Also renames formal property cells\n");
-		log("($assert, $assume, $cover, $live, $fair, $check) that have private names,\n");
-		log("giving them public witness-trackable names.\n");
-		log("\n");
-		log("This ensures that, during formal verification, a solver-found trace can be\n");
-		log("fully specified using public hierarchical names, and that individual property\n");
-		log("results can be tracked by name in flows that support per-property reporting\n");
-		log("(e.g. SBY with abc pdr in --keep-going mode).\n");
+		log("Assigns auto-generated names to objects used in formal verification\n");
+		log("that do not have a public name. This applies to all formal property\n");
+		log("cells ($assert, $assume, $cover, $live, $fair, $check), $any*/$all*\n");
+		log("output wires, and their containing cells.\n");
 		log("\n");
 		log("\n");
 		log("    rename -hide [selection]\n");