let smtlib_string_sexpr_conv = { s_let = HString.mk_hstring "let"; s_forall = HString.mk_hstring "forall"; s_exists = HString.mk_hstring "exists"; s_div = HString.mk_hstring "/"; s_minus = HString.mk_hstring "-"; s_define_fun = HString.mk_hstring "define-fun"; s_declare_fun = HString.mk_hstring "declare-fun"; prime_symbol = None; const_of_atom = const_of_smtlib_atom; symbol_of_atom = symbol_of_smtlib_atom; type_of_sexpr = type_of_smtlib_sexpr; expr_of_string_sexpr = gen_expr_of_string_sexpr'; expr_or_lambda_of_string_sexpr = gen_expr_or_lambda_of_string_sexpr' }