passing timeout option

leanprover-community · Dec 2, 2024 · 436da90 · 436da90
1 parent 28de206
commit 436da90
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean
@@ -145,13 +145,15 @@ def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := d
           let o := disableAllSolvers o
           let o := auto.smt.set o true
           let o := auto.smt.solver.name.set o sn
+          let o := auto.smt.timeout.set o config.timeout
           let o := auto.smt.trust.set o true
           o) <| runAutoOnConst name
       | .tptp sn path =>
         withOptions (fun o =>
           let o := disableAllSolvers o
           let o := auto.tptp.set o true
           let o := auto.tptp.solver.name.set o sn
+          let o := auto.tptp.timeout.set o config.timeout
           let o := auto.tptp.trust.set o true
           match sn with
           | .zipperposition => auto.tptp.zipperposition.path.set o path