Z3_ast Z3_API Z3_get_model_func_else(Z3_context c, Z3_model m, unsigned i) {
     Z3_TRY;
     LOG_Z3_get_model_func_else(c, m, i);
     RESET_ERROR_CODE();
     CHECK_NON_NULL(m, 0);
     Z3_func_decl d = get_model_func_decl_core(c, m, i);
     if (d) {
         model * _m = to_model_ref(m);
         func_interp * g = _m->get_func_interp(to_func_decl(d));
         if (g) {
             expr * e = g->get_else();
             mk_c(c)->save_ast_trail(e);
             RETURN_Z3(of_ast(e));
         }
         SET_ERROR_CODE(Z3_IOB);
         RETURN_Z3(0);
     }
     RETURN_Z3(0);
     Z3_CATCH_RETURN(0);
 }

 Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p) {
     Z3_TRY;
     LOG_Z3_tactic_apply_ex(c, t, g, p);
     RESET_ERROR_CODE();
     param_descrs pd;
     to_tactic_ref(t)->collect_param_descrs(pd);
     to_param_ref(p).validate(pd);
     Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p));
     RETURN_Z3(r);
     Z3_CATCH_RETURN(0);
 }

 Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c) {
     Z3_TRY;
     LOG_Z3_mk_fixedpoint(c);
     RESET_ERROR_CODE();
     Z3_fixedpoint_ref * d = alloc(Z3_fixedpoint_ref, *mk_c(c));
     d->m_datalog = alloc(api::fixedpoint_context, mk_c(c)->m(), mk_c(c)->fparams());
     mk_c(c)->save_object(d);
     Z3_fixedpoint r = of_datalog(d);
     RETURN_Z3(r);
     Z3_CATCH_RETURN(nullptr);
 }

 Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i) {
     Z3_TRY;
     LOG_Z3_get_smtlib_assumption(c, i);
     RESET_ERROR_CODE();
     if (mk_c(c)->m_smtlib_parser) {
         if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms()) {
             ast * a = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_axioms()[i];
             mk_c(c)->save_ast_trail(a);
             RETURN_Z3(of_ast(a));
         }
         else {
             SET_ERROR_CODE(Z3_IOB);
         }
     }
     else {
         SET_ERROR_CODE(Z3_NO_PARSER);
     }
     RETURN_Z3(0);
     Z3_CATCH_RETURN(0);
 }

 Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context target) {
     Z3_TRY;
     LOG_Z3_model_translate(c, m, target);
     RESET_ERROR_CODE();
     Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target));
     ast_translation tr(mk_c(c)->m(), mk_c(target)->m());
     dst->m_model = to_model_ref(m)->translate(tr);
     mk_c(target)->save_object(dst);
     RETURN_Z3(of_model(dst));
     Z3_CATCH_RETURN(nullptr);
 }

 Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t) {
     Z3_TRY;
     LOG_Z3_tactic_get_param_descrs(c, t);
     RESET_ERROR_CODE();
     Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
     mk_c(c)->save_object(d);
     to_tactic_ref(t)->collect_param_descrs(d->m_descrs);
     Z3_param_descrs r = of_param_descrs(d);
     RETURN_Z3(r);
     Z3_CATCH_RETURN(0);
 }

 Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s) {
     Z3_TRY;
     LOG_Z3_mk_fpa_to_fp_bv(c, bv, s);
     RESET_ERROR_CODE();
     if (!is_bv(c, bv) || !is_fp_sort(c, s)) {
         SET_ERROR_CODE(Z3_INVALID_ARG, "bv then fp sort expected");
         RETURN_Z3(nullptr);
     }
     api::context * ctx = mk_c(c);
     fpa_util & fu = ctx->fpautil();
     if (!ctx->bvutil().is_bv(to_expr(bv)) ||
         !fu.is_float(to_sort(s))) {
         SET_ERROR_CODE(Z3_INVALID_ARG, "bv sort the flaot sort expected");
         return nullptr;
     }
     expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv));
     ctx->save_ast_trail(a);
     RETURN_Z3(of_expr(a));
     Z3_CATCH_RETURN(nullptr);
 }

 Z3_solver Z3_API Z3_solver_translate(Z3_context c, Z3_solver s, Z3_context target) {
     Z3_TRY;
     LOG_Z3_solver_translate(c, s, target);
     RESET_ERROR_CODE();
     params_ref const& p = to_solver(s)->m_params; 
     Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
     sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
     mk_c(target)->save_object(sr);
     Z3_solver r = of_solver(sr);
     RETURN_Z3(r);
     Z3_CATCH_RETURN(0);
 }

 Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) {
     Z3_TRY;
     LOG_Z3_goal_translate(c, g, target);
     RESET_ERROR_CODE();
     ast_translation translator(mk_c(c)->m(), mk_c(target)->m());
     Z3_goal_ref * _r = alloc(Z3_goal_ref);
     _r->m_goal       = to_goal_ref(g)->translate(translator);
     mk_c(target)->save_object(_r);
     Z3_goal r = of_goal(_r);
     RETURN_Z3(r);
     Z3_CATCH_RETURN(0);
 }

 Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits) {
     Z3_TRY;
     LOG_Z3_mk_bv_numeral(c, sz, bits);
     RESET_ERROR_CODE();
     rational r(0);
     for (unsigned i = 0; i < sz; ++i) {
         if (bits[i]) r += rational::power_of_two(i);
     }
     ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz));
     RETURN_Z3(of_ast(a));
     Z3_CATCH_RETURN(nullptr);
 }

 Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f) {
     Z3_TRY;
     LOG_Z3_func_interp_get_else(c, f);
     RESET_ERROR_CODE();
     CHECK_NON_NULL(f, nullptr);
     expr * e = to_func_interp_ref(f)->get_else();
     if (e) {
         mk_c(c)->save_ast_trail(e);
     }
     RETURN_Z3(of_expr(e));
     Z3_CATCH_RETURN(nullptr);
 }

 Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i) {
     Z3_TRY;
     LOG_Z3_param_descrs_get_name(c, p, i);
     RESET_ERROR_CODE();
     if (i >= to_param_descrs_ptr(p)->size()) {
         SET_ERROR_CODE(Z3_IOB);
         RETURN_Z3(0);
     }
     Z3_symbol result = of_symbol(to_param_descrs_ptr(p)->get_param_name(i));
     return result;
     Z3_CATCH_RETURN(0);
 }

 Z3_ast Z3_API Z3_get_context_assignment(Z3_context c) {
     Z3_TRY;
     LOG_Z3_get_context_assignment(c);
     RESET_ERROR_CODE();
     ast_manager& m = mk_c(c)->m();
     expr_ref result(m);
     expr_ref_vector assignment(m);
     mk_c(c)->get_smt_kernel().get_assignments(assignment);
     result = mk_c(c)->mk_and(assignment.size(), assignment.c_ptr());
     RETURN_Z3(of_ast(result.get()));
     Z3_CATCH_RETURN(0);
 }

 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s) {
     Z3_TRY;
     LOG_Z3_solver_get_statistics(c, s);
     RESET_ERROR_CODE();
     init_solver(c, s);
     Z3_stats_ref * st = alloc(Z3_stats_ref);
     to_solver_ref(s)->collect_statistics(st->m_stats);
     mk_c(c)->save_object(st);
     Z3_stats r = of_stats(st);
     RETURN_Z3(r);
     Z3_CATCH_RETURN(0);
 }

 Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i) {
     Z3_TRY;
     LOG_Z3_get_smtlib_sort(c, i);
     RESET_ERROR_CODE(); 
     if (mk_c(c)->m_smtlib_parser) {
         mk_c(c)->extract_smtlib_parser_decls();
         if (i < mk_c(c)->m_smtlib_parser_sorts.size()) {
             sort* s = mk_c(c)->m_smtlib_parser_sorts[i];
             mk_c(c)->save_ast_trail(s);
             RETURN_Z3(of_sort(s));
         }
         else {
             SET_ERROR_CODE(Z3_IOB);
         }
     }
     else {
         SET_ERROR_CODE(Z3_NO_PARSER);
     }
     RETURN_Z3(0);
     Z3_CATCH_RETURN(0);
 }

 Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i) {
     Z3_TRY;
     LOG_Z3_get_smtlib_decl(c, i);
     RESET_ERROR_CODE(); 
     mk_c(c)->extract_smtlib_parser_decls();
     if (mk_c(c)->m_smtlib_parser) {
         if (i < mk_c(c)->m_smtlib_parser_decls.size()) {
             func_decl * d = mk_c(c)->m_smtlib_parser_decls[i];
             mk_c(c)->save_ast_trail(d);
             RETURN_Z3(of_func_decl(d));
         }
         else {
             SET_ERROR_CODE(Z3_IOB);
         }
     }
     else {
         SET_ERROR_CODE(Z3_NO_PARSER);
     }
     RETURN_Z3(0);
     Z3_CATCH_RETURN(0);
 }

 Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val) {
     Z3_TRY;
     LOG_Z3_rcf_mk_rational(c, val);
     RESET_ERROR_CODE();
     reset_rcf_cancel(c);
     scoped_mpq q(rcfm(c).qm());
     rcfm(c).qm().set(q, val);
     rcnumeral r;
     rcfm(c).set(r, q);
     RETURN_Z3(from_rcnumeral(r));
     Z3_CATCH_RETURN(0);
 }

 Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name) {
     Z3_TRY;
     LOG_Z3_mk_probe(c, name);
     RESET_ERROR_CODE();
     probe_info * p = mk_c(c)->find_probe(symbol(name));
     if (p == 0) {
         SET_ERROR_CODE(Z3_INVALID_ARG);
         RETURN_Z3(0);
     }
     probe * new_p = p->get();
     RETURN_PROBE(new_p);
     Z3_CATCH_RETURN(0);
 }

 Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, 
                            Z3_ast const args[], unsigned k) {
     Z3_TRY;
     LOG_Z3_mk_atmost(c, num_args, args, k);
     RESET_ERROR_CODE();
     parameter param(k);
     pb_util util(mk_c(c)->m());
     ast* a = util.mk_at_most_k(num_args, to_exprs(args), k);
     mk_c(c)->save_ast_trail(a);
     check_sorts(c, a);
     RETURN_Z3(of_ast(a));
     Z3_CATCH_RETURN(0);
 }

 Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name) {
     Z3_TRY;
     LOG_Z3_mk_tactic(c, name);
     RESET_ERROR_CODE();
     tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
     if (t == 0) {
         SET_ERROR_CODE(Z3_INVALID_ARG);
         RETURN_Z3(0);
     }
     tactic * new_t = t->mk(mk_c(c)->m());
     RETURN_TACTIC(new_t);
     Z3_CATCH_RETURN(0);
 }