diff --git a/tests/bench/mvcgen/sym/baseline_add_sub_cancel.lean b/tests/bench/mvcgen/sym/baseline_add_sub_cancel.lean
index f3e94037e2..9519539cae 100644
--- a/tests/bench/mvcgen/sym/baseline_add_sub_cancel.lean
+++ b/tests/bench/mvcgen/sym/baseline_add_sub_cancel.lean
@@ -20,6 +20,6 @@ def Goal (n : Nat) : Prop := ∀ s post, post () s → Exec s (loop n) post
 set_option maxRecDepth 10000
 set_option maxHeartbeats 10000000
 
-#eval runBenchUsingSym ``Goal [``loop, ``step] solve
-  [100, 200, 300, 400, 500, 600, 700, 800, 900, 1000]
+#eval runBenchUsingSym ``Goal [``loop, ``step] (solve · *> return []) `(tactic| fail)
+  [100, 500, 1000]
   -- [1000]
diff --git a/tests/bench/mvcgen/sym/lib/Driver.lean b/tests/bench/mvcgen/sym/lib/Driver.lean
index f38d45ce11..78598555cc 100644
--- a/tests/bench/mvcgen/sym/lib/Driver.lean
+++ b/tests/bench/mvcgen/sym/lib/Driver.lean
@@ -9,8 +9,15 @@ import Lean.Elab
 
 open Lean Parser Meta Elab Tactic Sym
 
+def timeItMs (k : MetaM α) : MetaM (α × UInt64) := do
+  let startTime ← IO.monoNanosNow
+  let a ← k
+  let endTime ← IO.monoNanosNow
+  let ms := (endTime - startTime).toFloat / 1000000.0
+  return (a, ms.toUInt64)
+
 /-- Helper function for executing a tactic `k` for solving `$(goal) n`. -/
-def driver (goal : Name) (unfold : List Name) (n : Nat) (check := true) (k : MVarId → MetaM Unit) : MetaM Unit := do
+def driver (goal : Name) (unfold : List Name) (n : Nat) (discharge : MetaM (TSyntax `tactic)) (check := true) (k : MVarId → MetaM (List MVarId)) : MetaM Unit := do
   let mvar ← mkFreshExprMVar (mkApp (mkConst goal) (mkNatLit n))
 -- The following code uses `Sym.simp`, but it balloons in the kernel. TODO: Investigate with new semantic
 -- foundations. Use regular simp for now.
@@ -23,46 +30,54 @@ def driver (goal : Name) (unfold : List Name) (n : Nat) (check := true) (k : MVa
 --  let unfold := Syntax.SepArray.ofElems (unfold.toArray |>.map (Lean.mkIdent ·))
   let lemmas ← unfold.toArray |>.push goal |>.mapM fun n => `(simpLemma| $(Lean.mkIdent n):term)
   let unfold := Syntax.TSepArray.ofElems (sep := ",") lemmas
-  let ([mvarId], _) ← Lean.Elab.runTactic mvar.mvarId! (← `(tactic| simp only [$unfold,*])).raw {} {}
-    | throwError "FAILED!"
-  let startTime ← IO.monoNanosNow
-  k mvarId
-  let endTime ← IO.monoNanosNow
-  let ms := (endTime - startTime).toFloat / 1000000.0
-  if check then
-    let startTime ← IO.monoNanosNow
-    checkWithKernel (← instantiateExprMVars mvar)
-    let endTime ← IO.monoNanosNow
-    let kernelMs := (endTime - startTime).toFloat / 1000000.0
-    IO.println s!"goal_{n}: {ms} ms, kernel: {kernelMs} ms"
+  let (mvarId, _unfoldMs) ← timeItMs do
+    let ([mvarId], _) ← Lean.Elab.runTactic mvar.mvarId! (← `(tactic| simp only [$unfold,*])).raw {} {}
+      | throwError "FAILED!"
+    return mvarId
+  -- IO.println s!"time spent unfolding: {_unfoldMs} ms"
+  let (mvarIds, ms) ← timeItMs do k mvarId
+  let discharge ← discharge
+  let dischargePp ← PrettyPrinter.ppTactic discharge
+  let dischargeMs? ← OptionT.run <| do
+    guard !mvarIds.isEmpty
+    Prod.snd <$> timeItMs do
+      for mvarId in mvarIds do
+        let ([], _) ← Lean.Elab.runTactic mvarId discharge.raw {} {}
+          | throwError "{dischargePp} failed to solve {mvarId}"
+  let (expr, instMs) ← timeItMs (instantiateMVars mvar)
+  let (_, kernelMs) ← timeItMs (checkWithKernel expr)
+  let mut msg := s!"goal_{n}: {ms} ms"
+  if let some dischargeMs := dischargeMs? then
+    msg := msg ++ s!", {mvarIds.length} VCs by {dischargePp}: {dischargeMs} ms"
   else
-    IO.println s!"goal_{n}: {ms} ms"
+    msg := msg ++ s!", {mvarIds.length} VCs"
+  if instMs > 1000 then
+    msg := msg ++ s!", instantiate > 1000ms: {instMs} ms"
+  msg := msg ++ s!", kernel: {kernelMs} ms"
+  IO.println msg
 
-def solveUsingTactic (goal : Name) (unfold : List Name) (n : Nat) (solve : MetaM (TSyntax `tactic)) (check := true) : MetaM Unit := do
-  driver goal unfold n check fun mvarId => do
-    let ([], _) ← Lean.Elab.runTactic mvarId (← solve).raw {} {} | throwError "FAILED!"
+def solveUsingTactic (goal : Name) (unfold : List Name) (n : Nat) (solve : MetaM (TSyntax `tactic)) (discharge : MetaM (TSyntax `tactic)) (check := true) : MetaM Unit := do
+  driver goal unfold n discharge check fun mvarId => do
+    let (mvarIds, _) ← Lean.Elab.runTactic mvarId (← solve).raw {} {}
+    return mvarIds
 
 /--
 Solves a goal of the form `goal n` using the given tactic, where `n` ranges over `sizes`.
 `unfold` is a list of `simp` lemmas to apply in order to unfold `goal n`.
 For many benchmarks, this is `[step, loop]`.
 -/
-public def runBenchUsingTactic (goal : Name) (unfold : List Name) (solve : MetaM (TSyntax `tactic)) (sizes : List Nat) : MetaM Unit := do
-  IO.println "=== VCGen tests ==="
-  IO.println ""
+public def runBenchUsingTactic (goal : Name) (unfold : List Name) (solve : MetaM (TSyntax `tactic)) (discharge : MetaM (TSyntax `tactic)) (sizes : List Nat) : MetaM Unit := do
   for n in sizes do
-    solveUsingTactic goal unfold n solve
+    solveUsingTactic goal unfold n solve discharge
 
-def solveUsingSym (goal : Name) (unfold : List Name) (n : Nat) (solve : MVarId → SymM Unit) (check := true) : MetaM Unit := do
-  driver goal unfold n check fun mvarId => SymM.run do solve mvarId
+def solveUsingSym (goal : Name) (unfold : List Name) (n : Nat) (solve : MVarId → SymM (List MVarId)) (discharge : MetaM (TSyntax `tactic)) (check := true) : MetaM Unit := do
+  driver goal unfold n discharge check fun mvarId => SymM.run do solve mvarId
 
 /--
 Solves a goal of the form `goal n` using a `SymM` procedure, where `n` ranges over `sizes`.
 `unfold` is a list of `simp` lemmas to apply in order to unfold `goal n`.
 For many benchmarks, this is `[step, loop]`.
 -/
-public def runBenchUsingSym (goal : Name) (unfold : List Name) (solve : MVarId → SymM Unit) (sizes : List Nat) : MetaM Unit := do
-  IO.println "=== Symbolic Simulation Tests ==="
-  IO.println ""
+public def runBenchUsingSym (goal : Name) (unfold : List Name) (solve : MVarId → SymM (List MVarId)) (discharge : MetaM (TSyntax `tactic)) (sizes : List Nat) : MetaM Unit := do
   for n in sizes do
-    solveUsingSym goal unfold n solve
+    solveUsingSym goal unfold n solve discharge
diff --git a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean
index 2212f13d95..489fe89acd 100644
--- a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean
+++ b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean
@@ -36,6 +36,6 @@ def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
 set_option maxRecDepth 10000
 set_option maxHeartbeats 10000000
 
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' <;> sorry)
-  [100, 200, 300, 400, 500, 600, 700, 800, 900, 1000]
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind)
+  [100, 500, 1000]
   -- [1000]
diff --git a/tests/bench/mvcgen/sym/vcgen_deep_add_sub_cancel.lean b/tests/bench/mvcgen/sym/vcgen_deep_add_sub_cancel.lean
index ce4ba0aae7..13adfa7f8a 100644
--- a/tests/bench/mvcgen/sym/vcgen_deep_add_sub_cancel.lean
+++ b/tests/bench/mvcgen/sym/vcgen_deep_add_sub_cancel.lean
@@ -57,6 +57,6 @@ example : Goal 20 := by
   mvcgen' <;> grind
 -/
 
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' <;> sorry)
-  [100, 200, 300, 400, 500, 600, 700, 800, 900, 1000]
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind)
+  [100, 500, 1000]
   -- [1000]
diff --git a/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean b/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
index 48650d076d..52ec487f65 100644
--- a/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
+++ b/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
@@ -37,6 +37,6 @@ example : Goal 20 := by
   all_goals sorry
 -/
 
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' <;> sorry)
-  [100, 200, 300, 400, 500, 600, 700, 800, 900, 1000]
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry)
+  [100, 500, 1000]
   -- [1000]