Fix heartbeat bug

leanprover-community · Feb 15, 2025 · efd479f · efd479f
1 parent d5dda92
commit efd479f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Duper/Interface.lean b/Duper/Interface.lean
@@ -402,7 +402,7 @@ def runDuper (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMax
         -- Add the constant `skolemSorry` to the environment
         let skSorryName ← addSkolemSorry
         let (_, state) ←
-          ProverM.runWithExprs (ctx := {startTime := ← IO.monoMsNow, initHeartbeats := ← getInitHeartbeats})
+          ProverM.runWithExprs (ctx := {startTime := ← IO.monoMsNow, initHeartbeats := ← IO.getNumHeartbeats})
             (s := {instanceMaxHeartbeats := instanceMaxHeartbeats, skolemSorryName := skSorryName})
             (ProverM.saturateNoPreprocessingClausification generateDatatypeExhaustivenessFacts)
             formulas

diff --git a/Main.lean b/Main.lean
@@ -25,7 +25,7 @@ def runDuperOnTPTP (fileName : String) (formulas : List (Expr × Expr × Array N
         -- Add the constant `skolemSorry` to the environment
         let skSorryName ← addSkolemSorry
         let (_, state) ←
-          ProverM.runWithExprs (ctx := {startTime := ← IO.monoMsNow, initHeartbeats := ← getInitHeartbeats})
+          ProverM.runWithExprs (ctx := {startTime := ← IO.monoMsNow, initHeartbeats := ← IO.getNumHeartbeats})
             (s := {instanceMaxHeartbeats := instanceMaxHeartbeats, skolemSorryName := skSorryName})
             (ProverM.saturateNoPreprocessingClausification generateDatatypeExhaustivenessFacts)
             formulas