We increase the reasoning power of the Record&Play algorithm for structural FSM traversal by incorporating a constraint-satisfying simulation technique. Combinational verification tools often use simulation to identify candidates for internally equivalent functions. This can significantly reduce the computational costs of prooving the equivalence of two circuits. The key idea to improve Record&Play is to perform a random simulation in every time frame that satisfies stored equivalences and constants which are needed to represent the state set. Our experimental results show the benefit of the proposed approach.