checkpointing revised encoding
streamlined SMT encoding---no more closure conversion needed