Add/test push/pop symbolic idempotence; some other optimizations