diff --git a/tests/bench/mvcgen/add_if_sub_StateM.lean b/tests/bench/mvcgen/add_if_sub_StateM.lean
new file mode 100644
index 0000000000..ff66ac0a6f
--- /dev/null
+++ b/tests/bench/mvcgen/add_if_sub_StateM.lean
@@ -0,0 +1,82 @@
+import Lean
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+/-!
+Same benchmark as `shallow_add_sub_cancel` but using `mvcgen`.
+-/
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  set (v + s)
+  let s' ← get
+  if s' = s then
+    set (s' - v)
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ∀ s₁, ⦃fun s => ⌜s = s₁⌝⦄ loop n ⦃⇓_ s₂ => ⌜s₂ > s₁⌝⦄
+
+open Lean Meta Elab
+
+/-- Helper function for executing a tactic `k` for solving `Goal n`. -/
+def driver (n : Nat) (check := true) (k : MVarId → MetaM Unit) : MetaM Unit := do
+  let some goal ← unfoldDefinition? (mkApp (mkConst ``Goal) (mkNatLit n)) | throwError "UNFOLD FAILED!"
+  let mvar ← mkFreshExprMVar goal
+  let startTime ← IO.monoNanosNow
+  k mvar.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"
+  else
+    IO.println s!"goal_{n}: {ms} ms"
+
+/-!
+`MetaM` Solution
+-/
+
+/-
+A tactic for solving goal `Goal n`
+-/
+macro "solve" : tactic => `(tactic| {
+  intro s₁
+  mvcgen -trivial [loop, step]
+  with grind
+})
+
+/--
+Solves a goal of the form `Goal n` using the `solve` tactic.
+-/
+def solveUsingMeta (n : Nat) (check := true) : MetaM Unit := do
+  driver n check fun mvarId => do
+    let ([], _) ← runTactic mvarId (← `(tactic| solve)).raw {} {} | throwError "FAILED!"
+
+def runBenchUsingMeta : MetaM Unit := do
+  IO.println "=== Symbolic Simulation Tests ==="
+  IO.println ""
+  for n in [2:6] do
+    solveUsingMeta n
+
+set_option maxRecDepth 10000
+set_option maxHeartbeats 10000000
+/--
+info: === Symbolic Simulation Tests ===
+
+goal_2: 99.023526 ms, kernel: 20.580785 ms
+goal_3: 188.955486 ms, kernel: 37.464098 ms
+goal_4: 436.369632 ms, kernel: 74.872961 ms
+goal_5: 1071.272357 ms, kernel: 148.864428 ms
+-/
+#guard_msgs in
+#eval runBenchUsingMeta
diff --git a/tests/bench/mvcgen/add_sub_cancel_StateM.lean b/tests/bench/mvcgen/add_sub_cancel_StateM.lean
new file mode 100644
index 0000000000..bf5d9682d3
--- /dev/null
+++ b/tests/bench/mvcgen/add_sub_cancel_StateM.lean
@@ -0,0 +1,99 @@
+import Lean
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+/-!
+Same benchmark as `shallow_add_sub_cancel` but using `mvcgen`.
+-/
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  set (s + v)
+  let s ← get
+  set (s - v)
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
+
+open Lean Meta Elab
+
+/-- Helper function for executing a tactic `k` for solving `Goal n`. -/
+def driver (n : Nat) (check := true) (k : MVarId → MetaM Unit) : MetaM Unit := do
+  let some goal ← unfoldDefinition? (mkApp (mkConst ``Goal) (mkNatLit n)) | throwError "UNFOLD FAILED!"
+  let mvar ← mkFreshExprMVar goal
+  let startTime ← IO.monoNanosNow
+  k mvar.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"
+  else
+    IO.println s!"goal_{n}: {ms} ms"
+
+/-!
+`MetaM` Solution
+-/
+
+/-
+A tactic for solving goal `Goal n`
+-/
+macro "solve" : tactic => `(tactic| {
+  intro post
+  mvcgen -trivial [loop, step]
+  with grind
+})
+
+/--
+Solves a goal of the form `Goal n` using the `solve` tactic.
+-/
+def solveUsingMeta (n : Nat) (check := true) : MetaM Unit := do
+  driver n check fun mvarId => do
+    let ([], _) ← runTactic mvarId (← `(tactic| solve)).raw {} {} | throwError "FAILED!"
+
+def runBenchUsingMeta (sizes : List Nat) : MetaM Unit := do
+  IO.println "=== Symbolic Simulation Tests ==="
+  IO.println ""
+  for n in sizes do
+    solveUsingMeta n
+
+set_option maxRecDepth 10000
+set_option maxHeartbeats 10000000
+/-
+info: === Symbolic Simulation Tests ===
+
+goal_10: 245.576221 ms, kernel: 134.134182 ms
+goal_20: 613.945320 ms, kernel: 115.453811 ms
+goal_30: 1074.053596 ms, kernel: 179.076070 ms
+goal_40: 1680.678302 ms, kernel: 252.066677 ms
+goal_50: 2457.209584 ms, kernel: 293.974096 ms
+goal_60: 3271.773330 ms, kernel: 368.394386 ms
+goal_70: 3981.247921 ms, kernel: 434.297822 ms
+goal_80: 5077.300540 ms, kernel: 507.047772 ms
+goal_90: 6486.990060 ms, kernel: 556.952095 ms
+goal_100: 7791.399986 ms, kernel: 623.605163 ms
+-/
+#guard_msgs in
+#eval runBenchUsingMeta [10, 20, 30, 40, 50, 60, 70, 80, 90, 100]
+
+/-
+#eval runBenchUsingMeta [30]
+
+example : Goal 10 := by
+  intro post
+  set_option trace.Elab.Tactic.Do.spec true in
+  mvcgen -trivial [loop, step]
+
+  simp [*]
+  -- with grind
+-/