let s_define_fun = smtlib_string_sexpr_conv.s_define_fun