class Z3::UninterpretedExpr