Need to specify sat tactic for Z3 solver.
Add checkpointing to Bool2CNFTranslator.
CheckpointableSolver needs to be a public interface.