Function visit_unique 

pub(crate) fn visit_unique<'a, B>(
    word: Option<&'a SymExpr>,
    condition: Option<&'a SymBoolExpr>,
    visitor: impl FnMut(&SymExpr) -> ControlFlow<B>,
) -> ControlFlow<B>

Visits reachable word nodes in depth-first, left-to-right order until the visitor breaks.

Expressions are hash-consed DAGs, so each distinct node is visited once. A tree walk would revisit shared subexpressions, which grows exponentially along chains such as nested hashes.