*smt-types*
ACL2 type functions and their corresponding Z3 type declarations.
Definition: *smt-types*
(defconst *smt-types*
'((realp . "_SMT_.RealSort()")
(rationalp . "_SMT_.RealSort()")
(integerp . "_SMT_.IntSort()")
(booleanp . "_SMT_.BoolSort()")
(symbolp . "Symbol_z3.z3Sym")))