diff --git a/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean b/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean
index 1229e9b730..3fb60fd78e 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean
@@ -6,6 +6,7 @@ open Lean Meta Elab Tactic Sym Std Do SpecAttr
 namespace GetThrowSet
 
 set_option mvcgen.warning false
+set_option backward.do.legacy false -- exercises asymmetric bind depth from new do elaborator
 
 abbrev M := ExceptT String <| StateM Nat
 
diff --git a/tests/bench/mvcgen/sym/lib/VCGen.lean b/tests/bench/mvcgen/sym/lib/VCGen.lean
index 286e0b212b..fdaa387343 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen.lean
+++ b/tests/bench/mvcgen/sym/lib/VCGen.lean
@@ -876,11 +876,10 @@ meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
 meta def work (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
   let goal := { goal with mvarId }
-  let mut worklist := Std.Queue.empty.enqueue goal
+  let mut worklist := #[goal]
   repeat do
-    let some (goal, worklist') := worklist.dequeue? | break
-    let mut goal := goal
-    worklist := worklist'
+    let mut some goal := worklist.back? | break
+    worklist := worklist.pop
     let res ← solve goal.mvarId
     match res with
     | .noEntailment .. | .noProgramFoundInTarget .. =>
@@ -896,7 +895,7 @@ meta def work (goal : Grind.Goal) : VCGenM Unit := do
       -- to share E-graph context before forking.
       if subgoals.length > 1 then
         goal ← (← read).preTac.processHypotheses goal
-      worklist := worklist.enqueueAll (subgoals.map ({ goal with mvarId := · }))
+      worklist := worklist ++ (subgoals |>.map ({ goal with mvarId := · }) |>.reverse)
 
 public structure Result where
   invariants : Array MVarId