Z3.Painless
class
Z3Symbol
a
data
Ty
ty2sort
const
script