From e6e878a98a5cef068a23ad44fa25dde99521c08c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 5 Apr 2026 02:01:57 +0000
Subject: [PATCH] fstar: clarify README relationship table heading per review

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/46fcd3bf-be90-4098-8516-fde0f1e37cbf

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 fstar/README.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/fstar/README.md b/fstar/README.md
index 1bc56151b..73bbfa50c 100644
--- a/fstar/README.md
+++ b/fstar/README.md
@@ -110,8 +110,7 @@ corresponding to the five `lemma_is_inf_to_fp_int_*` lemmas.
 
 ## Relationship to the C++ Code
 
-The following table maps each lemma to the corresponding C++ macro in
-`src/ast/rewriter/fpa_rewriter_rules.h` and where it is used.
+The following table maps each lemma to its corresponding C++ macro and the function where the macro is invoked.
 
 | Lemma | C++ macro | Used in |
 |---|---|---|