debugging small examples in --verify mode
checkpoint before removing Z3 datatype theory from encoding
incremental z3 queries; no longer using datatype theory; see unit-tests/unit1.fst for simple examples