static Z3_apply_result _tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g, params_ref p) {
        goal_ref new_goal;
        new_goal = alloc(goal, *to_goal_ref(g));
        Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, mk_c(c)->m());
        mk_c(c)->save_object(ref); 

        unsigned timeout     = p.get_uint("timeout", UINT_MAX);
        bool     use_ctrl_c  = p.get_bool("ctrl_c", false);
        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
        
        to_tactic_ref(t)->updt_params(p);

        api::context::set_interruptable si(*(mk_c(c)), eh);
        {
            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
            scoped_timer timer(timeout, &eh);
            try {
                exec(*to_tactic_ref(t), new_goal, ref->m_subgoals, ref->m_mc, ref->m_pc, ref->m_core);
                return of_apply_result(ref);
            }
            catch (z3_exception & ex) {
                mk_c(c)->handle_exception(ex);
                return 0;
            }
        }
    }

 void updt_params(params_ref const & p) {
     m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
     m_max_steps      = p.get_uint("max_steps", UINT_MAX);
     m_blast_add      = p.get_bool("blast_add", true);
     m_blast_mul      = p.get_bool("blast_mul", true);
     m_blast_full     = p.get_bool("blast_full", false);
     m_blast_quant    = p.get_bool("blast_quant", false);
     m_blaster.set_max_memory(m_max_memory);
 }

static void show_interpolant_and_maybe_check(cmd_context & ctx,
                                             ptr_vector<ast> &cnsts,
                                             expr *t, 
                                             ptr_vector<ast> &interps,
                                             params_ref &m_params,
                                             bool check)
{
  
    if (m_params.get_bool("som", false))
        m_params.set_bool("flat", true);
    th_rewriter s(ctx.m(), m_params);
  
    for(unsigned i = 0; i < interps.size(); i++){

        expr_ref r(ctx.m());
        proof_ref pr(ctx.m());
        s(to_expr(interps[i]),r,pr);

        ctx.regular_stream()  << mk_pp(r.get(), ctx.m()) << std::endl;
#if 0
        ast_smt_pp pp(ctx.m());
        pp.set_logic(ctx.get_logic().str().c_str());
        pp.display_smt2(ctx.regular_stream(), to_expr(interps[i]));
        ctx.regular_stream() << std::endl;
#endif
    }

    s.cleanup();

    // verify, for the paranoid...
    if(check || interp_params(m_params).check()){
        std::ostringstream err;
        ast_manager &_m = ctx.m();

        // need a solver -- make one here FIXME is this right?
        bool proofs_enabled, models_enabled, unsat_core_enabled;
        params_ref p;
        ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
        scoped_ptr<solver> sp = (ctx.get_solver_factory())(_m, p, false, true, false, ctx.get_logic());

        if(iz3check(_m,sp.get(),err,cnsts,t,interps))
            ctx.regular_stream() << "correct\n";
        else 
            ctx.regular_stream() << "incorrect: " << err.str().c_str() << "\n";
    }

    for(unsigned i = 0; i < interps.size(); i++){
        ctx.m().dec_ref(interps[i]);
    }

    interp_params itp_params(m_params);
    if(itp_params.profile())
        profiling::print(ctx.regular_stream());

}

void sls_engine::updt_params(params_ref const & _p) {
    sls_params p(_p);
    m_produce_models = _p.get_bool("model", false);
    m_max_restarts = p.max_restarts();
    m_tracker.set_random_seed(p.random_seed());
    m_walksat = p.walksat();
    m_walksat_repick = p.walksat_repick();
    m_paws_sp = p.paws_sp();
    m_paws = m_paws_sp < 1024;
    m_wp = p.wp();
    m_vns_mc = p.vns_mc();
    m_vns_repick = p.vns_repick();

    m_restart_base = p.restart_base();
    m_restart_next = m_restart_base;
    m_restart_init = p.restart_init();

    m_early_prune = p.early_prune();
    m_random_offset = p.random_offset();
    m_rescore = p.rescore();

    // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT.
    if (m_walksat_repick && !m_walksat)
        NOT_IMPLEMENTED_YET();
    if (m_vns_repick && !m_walksat)
        NOT_IMPLEMENTED_YET();
}

 void updt_params(params_ref const & _p) {
     sls_params p(_p);
     m_produce_models = _p.get_bool("model", false);
     m_max_restarts = p.restarts();            
     m_tracker.set_random_seed(p.random_seed());
     m_plateau_limit = p.plateau_limit();
 }

void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
    params.set_bool("magic_sets_for_queries", true);
    ast_manager m;
    random_gen ran(0);
    reg_decl_plugins(m);
    arith_util arith(m);
    const char * problem_dir = "C:\\tvm\\src\\z3_2\\debug\\test\\w0.datalog";
    dl_decl_util dl_util(m);

    std::cerr << "Testing queries on " << problem_dir <<"\n";
    register_engine re;
    context ctx(m, re, fparams);
    ctx.updt_params(params);
    {
        wpa_parser* p = wpa_parser::create(ctx, m);
        TRUSTME( p->parse_directory(problem_dir) );
        dealloc(p);
    }

    const unsigned attempts = 10;

    func_decl * v_pred = ctx.try_get_predicate_decl(symbol("V"));
    SASSERT(v_pred);
    sort * var_sort = v_pred->get_domain(0);

    uint64 var_sz;
    TRUSTME( ctx.try_get_sort_constant_count(var_sort, var_sz) );

    for(unsigned attempt=0; attempt<attempts; attempt++) {
        unsigned el1 = ran()%var_sz;
        unsigned el2 = ran()%var_sz;

        expr_ref_vector q_args(m);
        q_args.push_back(dl_util.mk_numeral(el1, var_sort));
        q_args.push_back(dl_util.mk_numeral(el2, var_sort));

        app_ref query_lit(m.mk_app(v_pred, q_args.c_ptr()), m);
        lbool is_sat = ctx.query(query_lit);
        SASSERT(is_sat != l_undef);
        bool found = is_sat == l_true;
        std::cerr<<"query finished: "<<found<<"\n";

        relation_fact ans_fact(m);
        ans_fact.push_back(to_app(q_args.back()));

        q_args.pop_back();
        q_args.push_back(m.mk_var(0, var_sort));

        query_lit = m.mk_app(v_pred, q_args.c_ptr());
        is_sat = ctx.query(query_lit.get());
        SASSERT(is_sat != l_false);
        std::cerr<<"non-ground query finished\n";
        if(ctx.result_contains_fact(ans_fact)!=found) {
            std::cerr<<"wrong wpa answer!\n";
            UNREACHABLE();
        }
    }

}

params_ref context_params::merge_default_params(params_ref const & p) {
    if (!m_auto_config && !p.contains("auto_config")) {
        params_ref new_p = p;
        new_p.set_bool("auto_config", false);
        return new_p;
    }
    else {
        return p;
    }
}

void smt_params::updt_local_params(params_ref const & _p) {
    smt_params_helper p(_p);
    m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams.
    m_random_seed = p.random_seed();
    m_relevancy_lvl = p.relevancy();
    m_ematching   = p.ematching();
    m_phase_selection = static_cast<phase_selection>(p.phase_selection());
    m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
    m_restart_factor = p.restart_factor();
    m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
    m_delay_units = p.delay_units();
    m_delay_units_threshold = p.delay_units_threshold();
    m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
    m_soft_timeout = p.soft_timeout();
    model_params mp(_p);
    m_model_compact = mp.compact();
    if (_p.get_bool("arith.greatest_error_pivot", false))
        m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
    else if (_p.get_bool("arith.least_error_pivot", false))
        m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
    theory_array_params::updt_params(_p);
}

 std::string get_value(char const * name) {
     std::string r;
     bool error = false;
     std::string error_msg;
     #pragma omp critical (gparams)
     {
         try {
             symbol m, p;
             normalize(name, m, p);
             if (m == symbol::null) {
                 if (m_params.contains(p)) {
                     r = get_value(m_params, p);
                 }
                 else {
                     r = get_default(get_param_descrs(), p, m);
                 }
             }
             else {
                 params_ref * ps = nullptr;
                 if (m_module_params.find(m, ps) && ps->contains(p)) {
                     r = get_value(*ps, p);
                 }
                 else {
                     param_descrs * d;
                     if (get_module_param_descrs().find(m, d)) {
                         r = get_default(*d, p, m);
                     }
                     else {
                         std::stringstream strm;
                         strm << "unknown module '" << m << "'";
                         throw exception(strm.str());
                     }
                 }
             }
         }
         catch (z3_exception & ex) {
             // Exception cannot cross critical section boundaries.
             error = true;
             error_msg = ex.msg();
         }
     }
     if (error)
         throw exception(std::move(error_msg));
     return r;
 }

 virtual void updt_params(params_ref const & p) {
     m_max_memory        = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
     m_aig_gate_encoding = p.get_bool("aig_default_gate_encoding", true);
     m_aig_per_assertion = p.get_bool("aig_per_assertion", true); 
 }

void context_params::updt_params(params_ref const & p) {
    m_timeout           = p.get_uint("timeout", UINT_MAX);
    m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
    m_auto_config       = p.get_bool("auto_config", true);
    m_proof             = p.get_bool("proof", false);
    m_model             = p.get_bool("model", true);
    m_model_validate    = p.get_bool("model_validate", false);
    m_trace             = p.get_bool("trace", false);
    m_trace_file_name   = p.get_str("trace_file_name", "z3.log");
    m_unsat_core        = p.get_bool("unsat_core", false);
    m_debug_ref_count   = p.get_bool("debug_ref_count", false);
    m_smtlib2_compliant = p.get_bool("smtlib2_compliant", false);
}

double params_ref::get_double(char const * k, params_ref const & fallback, double _default) const {
    return m_params ? m_params->get_double(k, fallback, _default) : fallback.get_double(k, _default);
}

 void updt_params(params_ref const & p) {
     m_fparams.m_nlquant_elim = p.get_bool(":qe-nonlinear", false);
     m_qe.updt_params(p);
 }

/**
   Update front_end_params using s.
   Only the most frequently used options are updated.

   This function is mainly used to allow smt::context to be used in
   the new strategy framework.
*/
void params2front_end_params(params_ref const & s, front_end_params & t) {
    t.m_quant_elim = s.get_bool(":elim-quant", t.m_quant_elim);
    t.m_relevancy_lvl = s.get_uint(":relevancy", t.m_relevancy_lvl);
    TRACE("qi_cost", s.display(tout); tout << "\n";);

void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) {
    proofs_enabled     = m.proofs_enabled() && p.get_bool("proof", m_proof);
    models_enabled     = p.get_bool("model", m_model);
    unsat_core_enabled = p.get_bool("unsat_core", m_unsat_core);
    p = merge_default_params(p);
}

 void updt_params_core(params_ref const & p) {
     m_normalize_int_only = p.get_bool("norm_int_only", true);
 }

bool params_ref::get_bool(char const * k, params_ref const & fallback, bool _default) const {
    return m_params ? m_params->get_bool(k, fallback, _default) : fallback.get_bool(k, _default);
}

void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) {
    m_max_memory        = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
    m_max_steps         = p.get_uint("max_steps", UINT_MAX);
    updt_local_params(p);
}

symbol params_ref::get_sym(char const * k, params_ref const & fallback, symbol const & _default) const {
    return m_params ? m_params->get_sym(k, fallback, _default) : fallback.get_sym(k, _default);
}

void bv2int_rewriter_ctx::update_params(params_ref const& p) {
    m_max_size = p.get_uint("max_bv_size", UINT_MAX);
}