diff --git a/fstar/README.md b/fstar/README.md
index 61ace6d92..69a719625 100644
--- a/fstar/README.md
+++ b/fstar/README.md
@@ -137,10 +137,13 @@ The three `let _ = run_tactic ...` blocks at the bottom of the file
 demonstrate extraction for the three ite-pushthrough lemmas and print
 their generated C++ to stdout during F* typechecking.
 
+### `../src/ast/rewriter/fpa_rewriter_rules.h`
 
-C++ header containing one `#define` macro per rewrite rule, extracted from
-the F\* lemmas.  Each macro is annotated with a `[extract: MACRO_NAME]`
-comment in the corresponding F\* lemma.
+C++ header containing one `#define` macro per rewrite rule, whose correctness
+is proved by F* lemmas in `FPARewriterRules.fst`.  The ite-pushthrough macros
+(`FPA_REWRITE_IS_NAN_ITE`, `FPA_REWRITE_IS_INF_ITE`, `FPA_REWRITE_IS_NORMAL_ITE`)
+can be regenerated by running `RewriteCodeGen.fst`.  Each macro is annotated
+with an `[extract: MACRO_NAME]` comment in the corresponding F* lemma.
 
 | Macro | F\* lemma(s) | Used in C++ function |
 |---|---|---|
diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst
index c6181a79c..459d6f9e5 100644
--- a/fstar/RewriteCodeGen.fst
+++ b/fstar/RewriteCodeGen.fst
@@ -105,7 +105,13 @@ let bvar_name (idx_map: list (nat & string)) (t: term) : Tac (option string) =
     let bvv = inspect_bv bv in
     (match List.Tot.assoc #nat bvv.index idx_map with
      | Some n -> Some n
-     | None -> Some (FStar.Sealed.unseal bvv.ppname))   (* fallback *)
+     | None ->
+       (* de Bruijn index not in our map; use the printer name as a fallback
+          and warn so the caller knows the index map may be incomplete. *)
+       let pp = FStar.Sealed.unseal bvv.ppname in
+       print ("WARNING: bvar_name fallback for index "
+              ^ string_of_int bvv.index ^ ", using ppname '" ^ pp ^ "'");
+       Some pp)
   | _ -> None
 
 (* Detect if-then-else in reflected terms.
@@ -425,18 +431,16 @@ let extract_rewrite (lemma: term) : Tac string =
 
 open FPARewriterRules
 
-(* Demonstrate extraction of the three ite-pushthrough lemmas. *)
-let _ =
-  run_tactic (fun () ->
-    print "\n=== lemma_is_nan_ite ===\n";
-    print (extract_rewrite (quote lemma_is_nan_ite)))
+(* Helper: extract and print one lemma's C++ rewrite rule. *)
+let print_rewrite (label: string) (lemma: term) : Tac unit =
+  print ("\n=== " ^ label ^ " ===\n");
+  print (extract_rewrite lemma)
 
+(* Demonstrate extraction of the three ite-pushthrough lemmas.
+   Running this file with F* prints the generated C++ for each rule. *)
 let _ =
   run_tactic (fun () ->
-    print "\n=== lemma_is_inf_ite ===\n";
-    print (extract_rewrite (quote lemma_is_inf_ite)))
-
-let _ =
-  run_tactic (fun () ->
-    print "\n=== lemma_is_normal_ite ===\n";
-    print (extract_rewrite (quote lemma_is_normal_ite)))
+    List.Tot.iter (fun (label, lemma) -> print_rewrite label lemma)
+      [ ("lemma_is_nan_ite",    quote lemma_is_nan_ite);
+        ("lemma_is_inf_ite",    quote lemma_is_inf_ite);
+        ("lemma_is_normal_ite", quote lemma_is_normal_ite) ])
diff --git a/src/ast/rewriter/fpa_rewriter_rules.h b/src/ast/rewriter/fpa_rewriter_rules.h
index c99611311..af12e2ce4 100644
--- a/src/ast/rewriter/fpa_rewriter_rules.h
+++ b/src/ast/rewriter/fpa_rewriter_rules.h
@@ -12,10 +12,10 @@ Abstract:
 
     The ite-pushthrough macros (FPA_REWRITE_IS_NAN_ITE, FPA_REWRITE_IS_INF_ITE,
     FPA_REWRITE_IS_NORMAL_ITE) can be regenerated programmatically by running
-    the Meta-F* extraction tactic in fstar/RewriteCodeGen.fst:
+    the Meta-F* extraction tactic in fstar/RewriteCodeGen.fst (from the repo root):
 
-      fstar.exe --include fstar fstar/IEEE754.fst \
-                fstar/FPARewriterRules.fst fstar/RewriteCodeGen.fst
+      cd /path/to/z3/fstar
+      fstar.exe --include . IEEE754.fst FPARewriterRules.fst RewriteCodeGen.fst
 
     The correspondence between each macro and the F* lemma it implements is
     documented at each macro definition below.