diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst
index b418f6aff..02400d5d8 100644
--- a/docs/source/using_yosys/more_scripting/model_checking.rst
+++ b/docs/source/using_yosys/more_scripting/model_checking.rst
@@ -136,14 +136,13 @@ names to all cells that participate in the witness framework:
 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
-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 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).
+The `write_aiger -ywmap` option generates a map file for conversion to and from
+Yosys witness traces, and also allows for mapping AIGER bad-state properties and
+invariant constraints back to individual formal properties by name. This enables
+features like 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
-``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.
+SMT2 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 836dfe5b1..a07d588c4 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -254,10 +254,9 @@ struct RenamePass : public Pass {
 		log("\n");
 		log("    rename -enumerate [-pattern <pattern>] [selection]\n");
 		log("\n");
-		log("Assign short auto-generated names to all selected wires and cells with private\n");
-		log("names. The -pattern option can be used to set the pattern for the new names.\n");
-		log("The character %% in the pattern is replaced with a integer number. The default\n");
-		log("pattern is '_%%_'.\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, $any*/$all* output wires, and their containing cells.\n");
 		log("\n");
 		log("\n");
 		log("    rename -witness\n");