From 176b761201ea21a75101199fd8c07b3395c44c4b Mon Sep 17 00:00:00 2001 From: etiennjf Date: Sat, 22 Nov 2025 11:06:42 +0100 Subject: [PATCH] set maxRecDepth to zero to avoid error during term elaboration --- Solver/Smt/Translate.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Solver/Smt/Translate.lean b/Solver/Smt/Translate.lean index 2dc9dc4..1a22ba9 100644 --- a/Solver/Smt/Translate.lean +++ b/Solver/Smt/Translate.lean @@ -88,10 +88,11 @@ def Translate.main (e : Expr) (logUndetermined := true) : TranslateEnvT (Result addAxioms (mkForall (← Term.mkFreshBinderName) BinderInfo.default a e) tl def command (sOpts: SolverOptions) (stx : Syntax) : TermElabM Unit := do - withRef stx do - instantiateMVars (← withSynthesize (postpone := .partial) <| elabTerm stx none) >>= fun e => do - let env := {(default : TranslateEnv) with optEnv.options.solverOptions := sOpts} - discard $ Translate.main e|>.run env + withTheReader Core.Context (fun ctx => { ctx with maxHeartbeats := 0, maxRecDepth := 0 }) $ do + withRef stx do + instantiateMVars (← withSynthesize (postpone := .partial) <| elabTerm stx none) >>= fun e => do + let env := {(default : TranslateEnv) with optEnv.options.solverOptions := sOpts} + discard $ Translate.main e|>.run env initialize registerTraceClass `Translate.expr