Augmenting transition systems for scalable symbolic model checking