⁵A reachability goal of the form ∃X₁,…,X_k s.t. s →^*t is linear if s is linear and s and t do not have variables in common.