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