diff --git a/tests/bench/sym/simp_1.lean b/tests/bench/sym/simp_1.lean
index b128e587bd..b5bc23ac42 100644
--- a/tests/bench/sym/simp_1.lean
+++ b/tests/bench/sym/simp_1.lean
@@ -10,7 +10,9 @@ namespace SimpBench
 def getProofSize (r : Sym.Simp.Result) : MetaM Nat :=
   match r with
   | .rfl _ _ => return 0
-  | .step _ p _ _ => p.numObjs
+  | .step _ p _ _ =>
+    let p := ShareCommon.shareCommon' p
+    p.numObjs
 
 def checkWithKernel (r : Sym.Simp.Result) : MetaM Float := do
   match r with
diff --git a/tests/elab/sym_simp_3.lean b/tests/elab/sym_simp_3.lean
index 7062859f45..014290f987 100644
--- a/tests/elab/sym_simp_3.lean
+++ b/tests/elab/sym_simp_3.lean
@@ -5,7 +5,7 @@ elab "sym_simp" "[" declNames:ident,* "]" : tactic => do
   let rewrite ← Sym.mkSimprocFor (← declNames.getElems.mapM fun s => realizeGlobalConstNoOverload s.raw) Sym.Simp.dischargeSimpSelf
   let methods : Sym.Simp.Methods := {
     pre  := Sym.Simp.simpControl
-    post := Sym.Simp.evalGround.andThen rewrite
+    post := Sym.Simp.evalGround >> rewrite
   }
   liftMetaTactic1 fun mvarId => Sym.SymM.run do
     let mvarId ← Sym.preprocessMVar mvarId