From c34e4cf0f74df54261cad75af833d28e98ae1c06 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 24 Dec 2025 00:22:12 +0100
Subject: [PATCH] perf: disable closed term extraction in bv_decide (#11785)

This PR disables closed term extraction in the reflection terms used by
`bv_decide`. These terms do
not profit at all from closed term extraction but can in practice cause
thousands of new closed term
declarations which in turn slows down the compiler.
---
 .../Elab/Tactic/BVDecide/Frontend/BVDecide.lean | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
index 3991a37f3d..e80328ded0 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
@@ -309,14 +309,15 @@ where
   Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
   -/
   mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
-    addAndCompile <| .defnDecl {
-      name := name,
-      levelParams := [],
-      type := type,
-      value := value,
-      hints := .abbrev,
-      safety := .safe
-    }
+    withOptions (fun opt => opt.setBool `compiler.extract_closed false) do
+      addAndCompile <| .defnDecl {
+        name := name,
+        levelParams := [],
+        type := type,
+        value := value,
+        hints := .abbrev,
+        safety := .safe
+      }
 
 def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :