test: use DFS ordering for subgoals in mvcgen (#13193)

This PR switches the mvcgen worklist from BFS (queue) to DFS (stack)
ordering for subgoal processing.

With the new do elaborator, `if`-without-`else` generates asymmetric
bind depth between branches (`pure () >>= cont` is optimized to just
`cont` in the else branch). This caused BFS-based VC numbering to depend
on elaborator internals, swapping vc10/vc11 in test cases. DFS ordering
follows the syntactic program structure more naturally and is robust to
such bind-depth asymmetries.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

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
 

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