This is implemented as a separate pass so that it can be understood
independently of the rest of the solver.