From 1d6b3d7dfa228b90c026e126737dcf3838a0413b Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Mon, 19 Jan 2026 16:44:09 -0600 Subject: [PATCH] Gather labels of cover statements in the procedure inlining transform --- Strata/Transform/ProcedureInlining.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean index 8f40ca34..e722fb14 100644 --- a/Strata/Transform/ProcedureInlining.lean +++ b/Strata/Transform/ProcedureInlining.lean @@ -102,7 +102,10 @@ def Statement.labels (s : Core.Statement) : List String := | .loop _ _ _ body _ => Block.labels body | .assume lbl _ _ => [lbl] | .assert lbl _ _ => [lbl] - | _ => [] + | .cover lbl _ _ => [lbl] + | .goto _ _ => [] + -- No other labeled commands. + | .cmd _ => [] termination_by s.sizeOf end @@ -128,7 +131,8 @@ def Statement.replaceLabels .loop g measure inv (Block.replaceLabels body map) m | .assume lbl e m => .assume (app lbl) e m | .assert lbl e m => .assert (app lbl) e m - | _ => s + | .cover lbl e m => .cover (app lbl) e m + | .cmd _ => s termination_by s.sizeOf end