THEORIES = builtin booleans uf arith bv fp arrays datatypes sep sets strings quantifiers idl