saveState and restoreState need to be called in logical pairs but are not. There is a commented-out invariant to verify this that does not pass.