Fix a typo in Sanity example
Allow to use SMT2's datatypes with --smt-data-types

This cannot be used when using --bottoms, since it assumes finite types
without loops.