diff --git a/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean b/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean index ceee64a96d..bcebf50ec7 100644 --- a/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean +++ b/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean @@ -15,5 +15,7 @@ set_option maxHeartbeats 100000000 -- Benchmark `mvcgen' with grind`: grind integrated into VCGen loop for incremental -- context internalization. This avoids O(n) re-internalization per VC. -#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail) +-- `simplifying_assumptions [Nat.add_assoc]` here speeds up grind and kernel checking by a factor +-- of 2 because long chains `s + 1 + ... + 1` are collapsed into `s + n`. +#eval runBenchUsingTactic ``GetThrowSetGrind.Goal [``loop, ``step] `(tactic| mvcgen' simplifying_assumptions [Nat.add_assoc] with grind) `(tactic| fail) [50, 100, 150]