SMTLib1

data Name

data Ident

data Quant

data Conn

data Formula

type Sort

data Binder

data Term

data Literal

data Annot

data FunDecl

data PredDecl

data Status

data Command

data Script

(===)

(=/=)

(.<.)

(.>.)

tInt

funDef

constDef

logic

assume

goal

class PP t