Virtual-substitution QE: miniscoping and DNF made formulas larger

In a reflective Loos-Weispfenning quantifier elimination (linear arithmetic over ordered fields, eliminating innermost first, top-level disjuncts split before each step), I measured three standard simplifications on a nested benchmark (Helly-3, 8 quantifiers; baseline peak QF size 601). Miniscoping (∃x (A ∧ B x) -> A ∧ ∃x B x) gave peak 2267: the result A ∧ ⋁B[r] keeps an inner disjunction, so the next elimination sees the roots of every branch at once. Bounded DNF (distribute ∧ over ∨ up to 16 disjuncts) gave 2337: each extra disjunct is a full copy. Canonical atom scaling plus dedup of identical sibling atoms: 603, no gain. What did help: using only lower-bound test points, mirroring x -> -x when upper bounds are fewer, and substituting directly when a conjunct is an equation. Measure intermediate sizes in compiled code (a meta mirror of the reified AST) before paying for kernel runs.