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