z3-src 415.4.4

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    smt_context.cpp

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-02-19.

Revision History:

--*/
#include<math.h>
#include "util/luby.h"
#include "util/warning.h"
#include "util/timeit.h"
#include "util/union_find.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_translation.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/proofs/proof_checker.h"
#include "ast/ast_util.h"
#include "ast/well_sorted.h"
#include "model/model_params.hpp"
#include "model/model.h"
#include "model/model_pp.h"
#include "smt/smt_context.h"
#include "smt/smt_quick_checker.h"
#include "smt/uses_theory.h"
#include "smt/theory_special_relations.h"
#include "smt/theory_polymorphism.h"
#include "smt/theory_sls.h"
#include "smt/smt_for_each_relevant_expr.h"
#include "smt/smt_model_generator.h"
#include "smt/smt_model_checker.h"
#include "smt/smt_model_finder.h"
#include "smt/smt_parallel.h"
#include "smt/smt_arith_value.h"
#include <iostream>

namespace smt {

    context::context(ast_manager & m, smt_params & p, params_ref const & _p):
        m(m),
        m_fparams(p),
        m_params(_p),
        m_setup(*this, p),
        m_relevancy_lvl(m_fparams.m_relevancy_lvl),
        m_asserted_formulas(m, p, _p),
        m_rewriter(m),
        m_qmanager(alloc(quantifier_manager, *this, p, _p)),
        m_model_generator(alloc(model_generator, m)),
        m_relevancy_propagator(mk_relevancy_propagator(*this)),
        m_user_propagator(nullptr),
        m_random(p.m_random_seed),
        m_flushing(false),
        m_lemma_id(0),
        m_progress_callback(nullptr),
        m_next_progress_sample(0),
        m_clause_proof(*this),
        m_fingerprints(m, m_region),
        m_b_internalized_stack(m),
        m_e_internalized_stack(m),
        m_l_internalized_stack(m),
        m_final_check_idx(0),
        m_cg_table(m),
        m_conflict(null_b_justification),
        m_not_l(null_literal),
        m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
        m_unsat_proof(m),
        m_dyn_ack_manager(*this, p),
        m_unknown("unknown"),
        m_unsat_core(m),
        m_mk_bool_var_trail(*this),
        m_mk_enode_trail(*this),
        m_mk_lambda_trail(*this),
        m_lemma_visitor(m) {

        SASSERT(m_scope_lvl == 0);
        SASSERT(m_base_lvl == 0);
        SASSERT(m_search_lvl == 0);

        m_case_split_queue = mk_case_split_queue(*this, p);
        m_rewriter.updt_params(m_asserted_formulas.get_params());

        init();

        if (!relevancy())
            m_fparams.m_relevancy_lemma = false;

        m_model_generator->set_context(this);
    }

    /**
       \brief retrieve flag for when cancelation is possible.
    */

    bool context::get_cancel_flag() {
        if (l_true == m_internal_completed && !m.limit().suspended()) {
            m_last_search_failure = CANCELED;
            return true;
        }
        if (m.limit().inc())
            return false;
        m_last_search_failure = CANCELED;
        return true;
    }

    void context::updt_params(params_ref const& p) {
        m_params.append(p);
        m_asserted_formulas.updt_params(p);
        if (!m_setup.already_configured()) {
            m_fparams.updt_params(p);
        }
    }

    unsigned context::relevancy_lvl() const {
        return std::min(m_relevancy_lvl, m_fparams.m_relevancy_lvl);
    }

    void context::copy(context& src_ctx, context& dst_ctx, bool override_base) {
        ast_manager& dst_m = dst_ctx.get_manager();
        ast_manager& src_m = src_ctx.get_manager();
        src_ctx.pop_to_base_lvl();

        if (!override_base && src_ctx.m_base_lvl > 0) {
            throw default_exception("Cloning contexts within a user-scope is not allowed");
        }
        SASSERT(src_ctx.m_base_lvl == 0 || override_base);

        ast_translation tr(src_m, dst_m, false);

        dst_ctx.set_logic(src_ctx.m_setup.get_logic());
        dst_ctx.copy_plugins(src_ctx, dst_ctx);

        asserted_formulas& src_af = src_ctx.m_asserted_formulas;
        asserted_formulas& dst_af = dst_ctx.m_asserted_formulas;

        // Copy asserted formulas.
        for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
            expr_ref fml(dst_m);
            proof_ref pr(dst_m);
            if (src_m.is_true(src_af.get_formula(i)))
               continue;
            proof* pr_src = src_af.get_formula_proof(i);
            fml = tr(src_af.get_formula(i));
            if (pr_src) {
                pr = tr(pr_src);
            }
            dst_af.assert_expr(fml, pr);
        }

        src_af.get_macro_manager().copy_to(dst_af.get_macro_manager());

        if (!src_ctx.m_setup.already_configured()) 
            return;

        for (unsigned i = 0; !src_m.proofs_enabled() && i < src_ctx.m_assigned_literals.size(); ++i) {
            literal lit = src_ctx.m_assigned_literals[i];
            bool_var_data const & d = src_ctx.get_bdata(lit.var());
            if (d.is_theory_atom() && !src_ctx.m_theories.get_plugin(d.get_theory())->is_safe_to_copy(lit.var())) {
                continue;
            }
            expr_ref fml0(src_m), fml1(dst_m);
            src_ctx.literal2expr(lit, fml0);
            if (src_m.is_true(fml0))
                continue;
            fml1 = tr(fml0.get());
            dst_ctx.assert_expr(fml1);
        }

        dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config);
        dst_ctx.internalize_assertions();
        
        dst_ctx.copy_user_propagator(src_ctx, true);

        TRACE(smt_context,
              src_ctx.display(tout);
              dst_ctx.display(tout););
    }

    context::~context() {
        flush();
        m_asserted_formulas.finalize();
    }

    void context::copy_plugins(context& src, context& dst) {
        // copy theory plugins
        for (theory* old_th : src.m_theory_set) {
            theory * new_th = old_th->mk_fresh(&dst);
            if (!new_th)
                throw default_exception("theory cannot be copied");
            dst.register_plugin(new_th);
        }
    }

    void context::copy_user_propagator(context& src_ctx, bool copy_registered) {
        if (!src_ctx.m_user_propagator) 
            return;
        auto* p = get_theory(m.mk_family_id("user_propagator"));
        m_user_propagator = reinterpret_cast<theory_user_propagator*>(p);
        SASSERT(m_user_propagator);
        if (!copy_registered) {
            return;
        }
        ast_translation tr(src_ctx.m, m, false);
        for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) {
            app* e = src_ctx.m_user_propagator->get_expr(i);
            m_user_propagator->add_expr(tr(e), true);
        }
    }

    context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) {
        context * new_ctx = alloc(context, m, p ? *p : m_fparams, pa);
        new_ctx->m_is_auxiliary = true;
        new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l);
        copy_plugins(*this, *new_ctx);
        new_ctx->copy_user_propagator(*this, false);
        return new_ctx;
    }

    void context::init() {
        app * t       = m.mk_true();
        mk_bool_var(t);
        SASSERT(get_bool_var(t) == true_bool_var);
        SASSERT(true_literal.var() == true_bool_var);
        m_assignment[true_literal.index()]     = l_true;
        m_assignment[false_literal.index()]    = l_false;
        if (m.proofs_enabled()) {
            proof * pr = m.mk_true_proof();

            set_justification(true_bool_var, m_bdata[true_bool_var], b_justification(mk_justification(justification_proof_wrapper(*this, pr))));
        }
        else {
            m_bdata[true_bool_var].set_axiom();
        }
        m_true_enode  = mk_enode(t, true, true, false);
        // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
        // m_true_enode->mark_as_interpreted();
        app * f       = m.mk_false();
        m_false_enode = mk_enode(f, true, true, false);
        // m_false_enode->mark_as_interpreted();
    }

    void context::set_progress_callback(progress_callback *cb) {
        m_progress_callback = cb;
    }

    /**
       \brief This method should be used to create equality atoms during the search.
       See comments in theory::mk_eq_atom
    */
    app * context::mk_eq_atom(expr * lhs, expr * rhs) {
        family_id fid = lhs->get_sort()->get_family_id();
        theory * th   = get_theory(fid);
        if (th)
            return th->mk_eq_atom(lhs, rhs);
        if (lhs->get_id() > rhs->get_id())
            std::swap(lhs, rhs);
        return m.mk_eq(lhs, rhs);
    }

    void context::set_justification(bool_var v, bool_var_data& d, b_justification const& j) {
        SASSERT(validate_justification(v, d, j));
        d.set_justification(j);
    }

    void context::assign_core(literal l, b_justification j, bool decision) {
        m_assigned_literals.push_back(l);
        m_assignment[l.index()]    = l_true;
        m_assignment[(~l).index()] = l_false;
        bool_var_data & d          = get_bdata(l.var());
        set_justification(l.var(), d, j);
        d.m_scope_lvl              = m_scope_lvl;
        if (m_fparams.m_restart_adaptive && d.m_phase_available) {
            m_agility             *= m_fparams.m_agility_factor;
            if (!decision && d.m_phase == l.sign())
                m_agility         += (1.0 - m_fparams.m_agility_factor);
        }
        d.m_phase_available        = true;
        d.m_phase                  = !l.sign();
        TRACE(assign_core, tout << (decision?"decision: ":"propagating: ") << l << " ";
              display_literal_smt2(tout, l) << "\n";
              tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
              display(tout, j);
              );
        TRACE(phase_selection, tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);

        if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l))) {
            m_atom_propagation_queue.push_back(l);
        }

        if (m.has_trace_stream())
            trace_assign(l, j, decision);

        m_case_split_queue->assign_lit_eh(l);
    }

    bool context::bcp() {
        SASSERT(!inconsistent());
        while (m_qhead < m_assigned_literals.size()) {
            if (get_cancel_flag()) {
                return true;
            }
            literal l      = m_assigned_literals[m_qhead];
            SASSERT(get_assignment(l) == l_true);
            m_qhead++;
            m_simp_counter--;
            literal not_l  = ~l;
            SASSERT(get_assignment(not_l) == l_false);
            watch_list & w = m_watches[l.index()];
            if (binary_clause_opt_enabled()) {
                // binary clause propagation
                b_justification js(l);
                literal * it  = w.begin_literals();
                literal * end = w.end_literals();
                for(; it != end; ++it) {
                    literal l = *it;
                    switch (get_assignment(l)) {
                    case l_false:
                        m_stats.m_num_bin_propagations++;
                        set_conflict(js, ~l);
                        return false;
                    case l_undef:
                        m_stats.m_num_bin_propagations++;
                        assign_core(l, js);
                        break;
                    case l_true:
                        break;
                    }
                }
            }

            // non-binary clause propagation
            watch_list::clause_iterator it  = w.begin_clause();
            watch_list::clause_iterator it2 = it;
            watch_list::clause_iterator end = w.end_clause();
            for(; it != end; ++it) {
                clause * cls = *it;
                CTRACE(bcp_bug, cls->get_literal(0) != not_l && cls->get_literal(1) != not_l, display_clause_detail(tout, cls);
                       tout << "not_l: "; display_literal(tout, not_l); tout << " " << not_l << "\n";);
                SASSERT(cls->get_literal(0) == not_l || cls->get_literal(1) == not_l);
                if (cls->get_literal(0) == not_l) {
                    cls->set_literal(0, cls->get_literal(1));
                    cls->set_literal(1, not_l);
                }

                SASSERT(cls->get_literal(1) == not_l);

                literal first_lit     = cls->get_literal(0);
                lbool   first_lit_val = get_assignment(first_lit);

                if (first_lit_val == l_true) {
                    *it2 = *it; // clause is already satisfied, keep it
                    it2++;
                }
                else {
                    literal * it3  = cls->begin() + 2;
                    literal * end3 = cls->end();
                    for(; it3 != end3; ++it3) {
                        if (get_assignment(*it3) != l_false) {
                            // swap literal *it3 with literal at position 0
                            // the negation of literal *it3 will watch clause cls.
                            m_watches[(~(*it3)).index()].insert_clause(cls);
                            cls->set_literal(1, *it3);
                            *it3   = not_l;
                            goto found_watch;
                        }
                    }
                    // did not find watch...
                    if (first_lit_val == l_false) {
                        // CONFLICT
                        // copy remaining watches
                        while (it < end) {
                            *it2 = *it;
                            it2++;
                            it++;
                        }
                        SASSERT(it2 <= end);
                        w.set_end_clause(it2);
                        SASSERT(is_empty_clause(cls));
                        set_conflict(b_justification(cls));
                        return false;
                    }
                    else {
                        // PROPAGATION
                        SASSERT(first_lit_val == l_undef);
                        SASSERT(get_assignment(first_lit) == l_undef);
                        SASSERT(is_unit_clause(cls));
                        *it2 = *it;
                        it2++; // keep clause
                        m_stats.m_num_propagations++;
                        // It is safe to call assign_core instead of assign because first_lit is unassigned
                        assign_core(first_lit, b_justification(cls));
                        if (m_fparams.m_relevancy_lemma && cls->is_lemma()) {
                            expr * e = bool_var2expr(first_lit.var());
                            // IMPORTANT: this kind of propagation asserts negative literals of the form (= A1 A2) where
                            // A1 and A2 are array terms. So, it may be interesting to disable it for array eqs.
                            //if (!(m.is_eq(e) && m.get_sort(to_app(e)->get_arg(0))->get_family_id() == m.get_family_id("array")))
                            mark_as_relevant(e);
                        }
                    }
                found_watch:;
                }
            }
            SASSERT(it2 <= end);
            w.set_end_clause(it2);
        }
        return true;
    }

    /**
       \brief Push a new equality for theory th, into the theory equality propagation queue.
    */
    void context::push_new_th_eq(theory_id th, theory_var lhs, theory_var rhs) {
        SASSERT(lhs != rhs);
        SASSERT(lhs != null_theory_var);
        SASSERT(rhs != null_theory_var);
        SASSERT(th != null_theory_id);
        SASSERT(get_theory(th)->get_enode(lhs) != get_theory(th)->get_enode(rhs));
        m_th_eq_propagation_queue.push_back(new_th_eq(th, lhs, rhs));
    }

    /**
       \brief Push a new disequality for theory th, into the theory disequality propagation queue.
    */
    void context::push_new_th_diseq(theory_id th, theory_var lhs, theory_var rhs) {
        SASSERT(lhs != rhs);
        SASSERT(lhs != null_theory_var);
        SASSERT(rhs != null_theory_var);
        SASSERT(th != null_theory_id);
        theory * t = get_theory(th);
        if (t->get_enode(lhs)->is_interpreted() && t->get_enode(rhs)->is_interpreted())
            return;
        TRACE(add_diseq,
              tout << "#" << t->get_enode(lhs)->get_owner_id() << " != "
              << "#" << t->get_enode(rhs)->get_owner_id() << "\n";);

        m_th_diseq_propagation_queue.push_back(new_th_eq(th, lhs, rhs));
    }

    class add_eq_trail : public trail {
        context& ctx;
        enode * m_r1;
        enode * m_n1;
        unsigned m_r2_num_parents;
    public:
        add_eq_trail(context& ctx, enode * r1, enode * n1, unsigned r2_num_parents):
            ctx(ctx),
            m_r1(r1),
            m_n1(n1),
            m_r2_num_parents(r2_num_parents) {
        }

        void undo() override {
            ctx.undo_add_eq(m_r1, m_n1, m_r2_num_parents);
        }
    };

    /**
       \brief Add the equality n1 = n2 with justification js into the logical context.
    */
    void context::add_eq(enode * n1, enode * n2, eq_justification js) {
        unsigned old_trail_size = m_trail_stack.size();
        scoped_suspend_rlimit _suspend_cancel(m.limit());

        try {
            TRACE(add_eq, tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
            TRACE(add_eq_detail, tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n";
                  tout << "kind: " << js.get_kind() << "\n";);
            SASSERT(n1->get_sort() == n2->get_sort());

            m_stats.m_num_add_eq++;
            enode * r1 = n1->get_root();
            enode * r2 = n2->get_root();

            if (r1 == r2) {
                TRACE(add_eq, tout << "redundant constraint.\n";);
                return;
            }
            IF_VERBOSE(20, verbose_stream() << "merge " << mk_bounded_pp(n1->get_expr(), m) << " " << mk_bounded_pp(n2->get_expr(), m) << "\n");

            if (r1->is_interpreted() && r2->is_interpreted()) {
                TRACE(add_eq, tout << "interpreted roots conflict.\n";);
                set_conflict(mk_justification(eq_conflict_justification(n1, n2, js)));
                return;
            }

            // Swap r1 and r2:
            //  1. if the "equivalence" class of r1 is bigger than the equivalence class of r2
            //  OR
            //  2. r1 is interpreted but r2 is not.
            //
            // The second condition is used to enforce the invariant that if a class contain
            // an interpreted enode then the root is also interpreted.
            if ((r1->get_class_size() > r2->get_class_size() && !r2->is_interpreted()) || r1->is_interpreted()) {
                SASSERT(!r2->is_interpreted());
                std::swap(n1, n2);
                std::swap(r1, r2);
            }

            TRACE(add_eq, tout << "merging: #" << r1->get_owner_id() << " #" << r2->get_owner_id() <<
                  " n1: #" << n1->get_owner_id() << "\n";);

            // It is necessary to propagate relevancy to other elements of
            // the equivalence class. This is necessary to enforce the invariant
            // in the field m_parent of the enode class.
            if (is_relevant(r1)) { // && !m.is_eq(r1->get_owner())) !is_eq HACK
                // NOTE for !is_eq HACK... the !is_eq HACK does not propagate relevancy when two
                // equality enodes are congruent. I tested this optimization because in V1
                // relevancy is not propagated for congruent equalities.
                // This occurs in V2, because we use the congruence table to propagate disequalities
                // efficiently.
                // I disabled this optimization HACK because it breaks invariants in the rest of the code.
                // To use it, I need to go over the code and analyze all affected places.
                mark_as_relevant(r2);
            }
            else if (is_relevant(r2)) { // && !m.is_eq(r2->get_owner())) { // !is_eq HACK
                mark_as_relevant(r1);
            }

            push_trail(add_eq_trail(*this, r1, n1, r2->get_num_parents()));

            m_qmanager->add_eq_eh(r1, r2);


            merge_theory_vars(n2, n1, js);

            // 'Proof' tree
            // n1 -> ... -> r1
            // n2 -> ... -> r2
            SASSERT(n1->trans_reaches(r1));
            invert_trans(n1);
            n1->m_trans.m_target        = n2;
            n1->m_trans.m_justification = js;
            n1->m_proof_is_logged   = false;
            SASSERT(r1->trans_reaches(n1));
            // ---------------
            // r1 -> ..  -> n1 -> n2 -> ... -> r2

            remove_parents_from_cg_table(r1);

            enode * curr = r1;
            do {
                curr->m_root = r2;
                curr = curr->m_next;
            }
            while(curr != r1);

            SASSERT(r1->get_root() == r2);
            reinsert_parents_into_cg_table(r1, r2, n1, n2, js);

            if (n2->is_bool())
                propagate_bool_enode_assignment(r1, r2, n1, n2);

            // Merge "equivalence" classes
            std::swap(r1->m_next, r2->m_next);

            // Update "equivalence" class size
            r2->m_class_size += r1->m_class_size;
            r2->m_is_shared = 2;

            CASSERT("add_eq", check_invariant());
        }
        catch (...) {
            // Restore trail size since procedure was interrupted in the middle.
            // If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
            TRACE(add_eq, tout << "add_eq interrupted. This is unsafe " << m.limit().is_canceled() << "\n";);
            m_trail_stack.shrink(old_trail_size);
            throw;
        }
    }

    /**
       \brief When merging to equivalence classes, the parents of the smallest one (that are congruence roots),
       must be removed from the congruence table since their hash code will change.
    */
    void context::remove_parents_from_cg_table(enode * r1) {
        // Remove parents from the congruence table
        for (enode * parent : enode::parents(r1)) {
            CTRACE(add_eq, !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";);
            CTRACE(add_eq, !parent->is_marked() && parent->is_cgc_enabled() && !parent->is_true_eq() &&  parent->is_cgr() && !m_cg_table.contains_ptr(parent), 
                   tout << "cgr !contains " << parent->get_owner_id() << " " << mk_pp(parent->get_decl(), m) << "\n";
                   for (enode* n : enode::args(parent))  tout << n->get_root()->get_owner_id() << " " << n->get_root()->hash() << " ";
                   tout << "\n";
                   tout << "contains: " << m_cg_table.contains(parent) << "\n";
                   if (m_cg_table.contains(parent)) {
                       tout << "owner: " << m_cg_table.find(parent)->get_owner_id() << "\n";
                   }
                   m_cg_table.display(tout);
                   );
            CTRACE(add_eq, !parent->is_marked() && parent->is_cgc_enabled() && !parent->is_true_eq() && !parent->is_cgr() &&  m_cg_table.contains_ptr(parent), tout << "!cgr contains " << parent->get_owner_id() << "\n";);
            SASSERT(parent->is_marked() || !parent->is_cgc_enabled() ||  parent->is_true_eq() || parent->is_cgr() == m_cg_table.contains_ptr(parent));
            SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || !parent->is_true_eq() || !m_cg_table.contains_ptr(parent));
            if (!parent->is_marked() && parent->is_cgr() && !parent->is_true_eq()) {
                SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent));
                parent->set_mark();
                if (parent->is_cgc_enabled()) {
                    m_cg_table.erase(parent);
                    SASSERT(!m_cg_table.contains_ptr(parent));
                }
            }
        }
    }

    /**
       \brief Reinsert the parents of r1 that were removed from the
       cg_table at remove_parents_from_cg_table. Some of these parents will
       become congruent to other enodes, and a new equality will be propagated.
       Moreover, this method is also used for doing equality propagation.

       The parents of r1 that remain as congruence roots are copied to the
       r2->m_parents.

       The n1, n2, js arguments are used to implement dynamic ackermanization.
       js is a justification for n1 and n2 being equal, and the equality n1 = n2 is
       the one that implied r1 = r2.
    */
    void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) {
        enode_vector & r2_parents  = r2->m_parents;
        enode_vector & r1_parents  = r1->m_parents;
        unsigned num_r1_parents = r1_parents.size();
        for (unsigned i = 0; i < num_r1_parents; ++i) {
            enode* parent = r1_parents[i];
            if (!parent->is_marked())
                continue;
            parent->unset_mark();
            if (parent->is_eq()) {
                SASSERT(parent->get_num_args() == 2);
                TRACE(add_eq_bug, tout << "visiting: #" << parent->get_owner_id() << "\n";);
                enode * lhs = parent->get_arg(0);
                enode * rhs = parent->get_arg(1);
                if (lhs->get_root() == rhs->get_root()) {
                    SASSERT(parent->is_true_eq());
                    unsigned expr_id = parent->get_owner_id();
                    bool_var v = get_bool_var_of_id(expr_id);
                    lbool val  = get_assignment(v);
                    if (val != l_true) {
                        if (val == l_false && js.get_kind() == eq_justification::CONGRUENCE)
                            m_dyn_ack_manager.cg_conflict_eh(n1->get_expr(), n2->get_expr());
                        assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs)));
                    }
                    // It is not necessary to reinsert the equality to the congruence table
                    continue;
                }
            }
            if (parent->is_cgc_enabled()) {
                enode_bool_pair pair = m_cg_table.insert(parent);
                enode * parent_prime = pair.first;
                if (parent_prime == parent) {
                    SASSERT(parent);
                    SASSERT(parent->is_cgr());
                    SASSERT(m_cg_table.contains_ptr(parent));
                    r2_parents.push_back(parent);
                    continue;
                }
                parent->m_cg = parent_prime;
                SASSERT(!m_cg_table.contains_ptr(parent));
                if (parent_prime->m_root != parent->m_root) {
                    bool used_commutativity = pair.second;
                    TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id()
                          << " used_commutativity: " << used_commutativity << "\n";);
                    push_new_congruence(parent, parent_prime, used_commutativity);
                }
            }
            else {
                // If congruence closure is not enabled for parent, then I just copy it
                // to r2_parents
                r2_parents.push_back(parent);
            }
        }
    }

    /**
       \brief A transitivity 'proof' branch is represented by
       the following sequence starting at n and ending
       at n->get_root.

       N1      = n
       N_{i+1} = N_i->m_trans.m_target
       and, there is an k such that N_k = n->get_root()

       This method will invert this branch.
    */
    void context::invert_trans(enode * n) {
        enode * curr                      = n->m_trans.m_target;
        enode * prev                      = n;
        eq_justification js               = n->m_trans.m_justification;
        prev->m_trans.m_target            = nullptr;
        prev->m_trans.m_justification     = null_eq_justification;
        prev->m_proof_is_logged       = false;
        while (curr != nullptr) {
            SASSERT(prev->trans_reaches(n));
            enode * new_curr              = curr->m_trans.m_target;
            eq_justification new_js       = curr->m_trans.m_justification;
            curr->m_trans.m_target        = prev;
            curr->m_trans.m_justification = js;
            curr->m_proof_is_logged   = false;
            prev                          = curr;
            js                            = new_js;
            curr                          = new_curr;
        }
    }

    /**
       \brief Given that r is the root of n, and r contains a theory variable
       for theory th_id, this method returns a theory variable that is 'closer'
       to n in the 'proof branch' n -> ... -> r.

       This method is used to improve the quality of the conflict clauses produced
       by the logical context.

       Consider the following example:

       - Consider the following sequence of equalities:
       n1 = n2 = n3 = n4 = n5 = n6

       - Now, assume that n1 is the root of the equivalence class
       after each merge. So, the 'proof' branch will have the following
       shape:

       n1 <- n2 <- n3 <- n4 <- n5 <- n6

       - Assuming that all nodes are attached to theory variable, then the following
       sequence of equalities is sent to the theory if the method get_closest_var is not used:

       n1 = n2, n1 = n3, n1 = n4, n1 = n5, n1 = n6

       - This sequence is bad, and bad justifications may be produced by theory.
       For example, assume the following arithmetic constraint

       n5 < n6

       For the arithmetic module, the best justification will be:
       n1 = n5, n1 = n6 and n5 < n6

       This justification contains unnecessary 'junk' to justify that n5 = n6.
       That is, it proves n5 = n6 using the proofs for n1 = n5 and n1 = n6.

       When the method get_closest_var is used in the communication with theories,
       the logical context will send the natural sequence of equalities to the theories:

       n1 = n2 = n3 = n4 = n5 = n6
    */
    theory_var context::get_closest_var(enode * n, theory_id th_id) {
        if (th_id == null_theory_id)
            return null_theory_var;
        while (n != nullptr) {
            theory_var v = n->get_th_var(th_id);
            if (v != null_theory_var)
                return v;
            n = n->m_trans.m_target;
        }
        return null_theory_var;
    }

    /**
       \brief Merge the theory variables of n2->get_root() and n1->get_root(), the result is stored in n2->get_root().
       New th_var equalities are propagated to the theories.

       \remark In most cases, an enode is attached to at most one theory var.
    */
    void context::merge_theory_vars(enode * n2, enode * n1, eq_justification js) {
        enode * r2 = n2->get_root();
        enode * r1 = n1->get_root();
        if (!r1->has_th_vars() && !r2->has_th_vars()) {
            TRACE(merge_theory_vars, tout << "Neither have theory vars #" 
                  << mk_bounded_pp(n1->get_expr(), m) << " #" << mk_bounded_pp(n2->get_expr(), m) << "\n";);
            return;
        }

        theory_id from_th = null_theory_id;

        if (js.get_kind() == eq_justification::JUSTIFICATION)
            from_th = js.get_justification()->get_from_theory();

        if (r2->m_th_var_list.get_next() == nullptr && r1->m_th_var_list.get_next() == nullptr) {
            // Common case: r2 and r1 have at most one theory var.
            theory_id  t2 = r2->m_th_var_list.get_id();
            theory_id  t1 = r1->m_th_var_list.get_id();
            theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : r2->m_th_var_list.get_var();
            theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_var();
            TRACE(merge_theory_vars,
                  tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id()
                  << ", t2: " << t2 << ", t1: " << t1 << "\n";);
            if (v2 != null_theory_var && v1 != null_theory_var) {
                if (t1 == t2) {
                    // only send the equality to the theory, if the equality was not propagated by it.
                    if (t1 != from_th)
                        push_new_th_eq(t1, v2, v1);
                }
                else {
                    // uncommon case: r2 will have two theory_vars attached to it.
                    r2->add_th_var(v1, t1, m_region);
                    push_new_th_diseqs(r2, v1, get_theory(t1));
                    push_new_th_diseqs(r1, v2, get_theory(t2));
                }
            }
            else if (v1 == null_theory_var && v2 != null_theory_var) {
                push_new_th_diseqs(r1, v2, get_theory(t2));
            }
            else if (v1 != null_theory_var && v2 == null_theory_var) {
                r2->m_th_var_list.set_var(v1);
                r2->m_th_var_list.set_id(t1);
                TRACE(merge_theory_vars, tout << "push_new_th_diseqs v1: " << v1 << ", t1: " << t1 << "\n";);
                push_new_th_diseqs(r2, v1, get_theory(t1));
            }
        }
        else {
            // r1 and/or r2 have more than one theory variable.
            TRACE(merge_theory_vars,
                  tout << "#" << r1->get_owner_id() << " == #" << r2->get_owner_id() << "\n";);


            theory_var_list * l2 = r2->get_th_var_list();
            while (l2) {
                theory_id  t2 = l2->get_id();
                theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : l2->get_var();
                SASSERT(v2 != null_theory_var);
                SASSERT(t2 != null_theory_id);
                theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t2) : r1->get_th_var(t2);

                TRACE(merge_theory_vars, tout << get_theory(t2)->get_name() << ": " << v2 << " == " << v1 << "\n");

                if (v1 != null_theory_var) {
                    // only send the equality to the theory, if the equality was not propagated by it.
                    if (t2 != from_th)
                        push_new_th_eq(t2, v2, v1);
                }
                else {
                    push_new_th_diseqs(r1, v2, get_theory(t2));
                }
                l2 = l2->get_next();
            }

            theory_var_list * l1 = r1->get_th_var_list();
            while (l1) {
                theory_id  t1 = l1->get_id();
                theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : l1->get_var();
                SASSERT(v1 != null_theory_var);
                SASSERT(t1 != null_theory_id);
                theory_var v2 = r2->get_th_var(t1);
                TRACE(merge_theory_vars, tout << get_theory(t1)->get_name() << ": " << v2 << " == " << v1 << "\n");
                if (v2 == null_theory_var) {
                    r2->add_th_var(v1, t1, m_region);
                    push_new_th_diseqs(r2, v1, get_theory(t1));
                }
                l1 = l1->get_next();
            }
        }
    }

    /**
       \brief Propagate the boolean assignment when two equivalence classes are merged.
    */
    void context::propagate_bool_enode_assignment(enode * r1, enode * r2, enode * n1, enode * n2) {
        SASSERT(n1->is_bool());
        SASSERT(n2->is_bool());
        SASSERT(r1->is_bool());
        SASSERT(r2->is_bool());
        if (r2 == m_false_enode || r2 == m_true_enode) {
            bool sign = r2 == m_false_enode;
            enode * curr = r1;
            do {
                SASSERT(curr != m_false_enode);
                bool_var v = enode2bool_var(curr);
                literal l(v, sign);
                CTRACE(propagate, (get_assignment(l) != l_true), tout << enode_pp(curr, *this) << " " << l << "\n");
                if (get_assignment(l) != l_true)
                    assign(l, mk_justification(eq_root_propagation_justification(curr)));
                curr = curr->m_next;
            }
            while (curr != r1);
        }
        else {
            bool_var v1 = enode2bool_var(n1);
            bool_var v2 = enode2bool_var(n2);
            lbool val1  = get_assignment(v1);
            lbool val2  = get_assignment(v2);
            if (val1 != val2) {
                if (val2 == l_undef)
                    propagate_bool_enode_assignment_core(n1, n2);
                else
                    propagate_bool_enode_assignment_core(n2, n1);
            }
        }
    }

    /**
       \brief source and target are boolean enodes, they were proved to be equal,
       and the boolean variable associated with source is assigned. Then,
       copy the assignment to the boolean variables associated with target.
    */
    void context::propagate_bool_enode_assignment_core(enode * source, enode * target) {
        SASSERT(source->is_bool());
        SASSERT(target->is_bool());
        SASSERT(source->get_root() == target->get_root());
        bool_var v_source = enode2bool_var(source);
        lbool    val      = get_assignment(v_source);
        SASSERT(val != l_undef);
        bool     sign     = val == l_false;
        enode * first = target;
        do {
            bool_var v2 = enode2bool_var(target);
            lbool val2  = get_assignment(v2);
            if (val2 != val) {
                if (val2 != l_undef && congruent(source, target) && source->get_num_args() > 0)
                    m_dyn_ack_manager.cg_conflict_eh(source->get_expr(), target->get_expr());
                assign(literal(v2, sign), mk_justification(mp_iff_justification(source, target)));
            }
            target = target->get_next();
        }
        while (first != target);
    }

    void context::undo_add_eq(enode * r1, enode * n1, unsigned r2_num_parents) {
        enode * r2 = r1->get_root();
        TRACE(add_eq, tout << "undo_add_eq #" << r1->get_owner_id() << " #" << r2->get_owner_id() << "\n";);

        // restore r2 class size
        r2->m_class_size -= r1->m_class_size;
        r2->m_is_shared = 2;

        // unmerge "equivalence" classes
        std::swap(r1->m_next, r2->m_next);

        // remove the parents of r1 that remained as congruence roots
        enode_vector::iterator it  = r2->begin_parents();
        enode_vector::iterator end = r2->end_parents();
        it += r2_num_parents;
        for (; it != end; ++it) {
            enode * parent = *it;
            if (parent->is_cgc_enabled()) {
                CTRACE(add_eq, !parent->is_cgr() || !m_cg_table.contains_ptr(parent),
                       tout << "old num_parents: " << r2_num_parents 
                            << "\nnum_parents: " << r2->m_parents.size() 
                            << "\nparent: #" << parent->get_owner_id() 
                            << "\nparents: ";
                       for (enode* p : r2->m_parents) tout << "#" << p->get_owner_id() << " ";
                       display(tout << "\n"););
                SASSERT(parent->is_cgr());
                SASSERT(m_cg_table.contains_ptr(parent));
                m_cg_table.erase(parent);
            }
        }

        enode * curr = r1;
        do {
            curr->m_root = r1;
            curr = curr->m_next;
        }
        while (curr != r1);

        // restore parents of r2
        r2->m_parents.shrink(r2_num_parents);

        // try to reinsert parents of r1 that are not cgr
        for (enode * parent : enode::parents(r1)) {
            TRACE(add_eq_parents, tout << "visiting: #" << parent->get_owner_id() << "\n";);
            if (parent->is_cgc_enabled()) {
                
                enode * cg = parent->m_cg;
                if (!parent->is_true_eq() &&
                    (parent == cg ||           // parent was root of the congruence class before and after the merge
                     !congruent(parent, cg)    // parent was root of the congruence class before but not after the merge
                     )) {
                    enode_bool_pair p = m_cg_table.insert(parent);
                    parent->m_cg = p.first;
                }
            }
        }

        // restore theory vars
        if (r2->m_th_var_list.get_next() == nullptr) {
            // common case: r2 has at most one variable
            theory_var v2 = r2->m_th_var_list.get_var();
            if (v2 != null_theory_var) {
                theory_id  t2 = r2->m_th_var_list.get_id();
                if (get_theory(t2)->get_enode(v2)->get_root() != r2) {
                    SASSERT(get_theory(t2)->get_enode(v2)->get_root() == r1);
                    r2->m_th_var_list.set_var(null_theory_var); //remove variable from r2
                    r2->m_th_var_list.set_id(null_theory_id);
                }
            }
        }
        else {
            restore_theory_vars(r2, r1);
        }

        // 'Proof' tree
        // r1 -> ..  -> n1 -> n2 -> ... -> r2
        SASSERT(r1->trans_reaches(r2));
        SASSERT(r1->trans_reaches(n1));
        n1->m_trans.m_target        = nullptr;
        n1->m_trans.m_justification = null_eq_justification;
        n1->m_proof_is_logged   = false;
        invert_trans(r1);
        // ---------------
        // n1 -> ... -> r1
        // n2 -> ... -> r2
        SASSERT(n1->trans_reaches(r1));
        SASSERT(r1->m_trans.m_target == 0);

        CASSERT("add_eq", check_invariant());
    }

    /**
       \brief Auxiliary method for undo_add_eq.
       It restores the theory variables of a given root enode.
       This method deletes any theory variable v2 of r2 (for a theory t2)
       whenever:

       get_theory(t2)->get_enode(v2)->get_root() != r2

       That is, v2 is not equivalent to r2 anymore.
    */
    void context::restore_theory_vars(enode * r2, enode * r1) {
        SASSERT(r2->get_root() == r2);
        theory_var_list * new_l2  = nullptr;
        theory_var_list * l2      = r2->get_th_var_list();
        while (l2) {
            theory_var v2 = l2->get_var();
            theory_id t2  = l2->get_id();

            if (get_theory(t2)->get_enode(v2)->get_root() != r2) {
                SASSERT(get_theory(t2)->get_enode(v2)->get_root() == r1);
                l2 = l2->get_next();
            }
            else {
                if (new_l2) {
                    new_l2->set_next(l2);
                    new_l2 = l2;
                }
                else {
                    r2->m_th_var_list = *l2;
                    new_l2 = &(r2->m_th_var_list);
                }
                l2 = l2->get_next();
            }
        }

        if (new_l2) {
            new_l2->set_next(nullptr);
        }
        else {
            r2->m_th_var_list.set_var(null_theory_var);
            r2->m_th_var_list.set_next(nullptr);
        }
    }

    /**
       \brief This method is invoked when a new disequality is asserted.
       The disequality is propagated to the theories.
    */
    bool context::add_diseq(enode * n1, enode * n2) {
        enode * r1 = n1->get_root();
        enode * r2 = n2->get_root();
        TRACE(add_diseq, tout << "assigning: #" << n1->get_owner_id() << " != #" << n2->get_owner_id() << "\n";
              tout << mk_ll_pp(n1->get_expr(), m) << " != ";
              tout << mk_ll_pp(n2->get_expr(), m) << "\n";
              tout << mk_ll_pp(r1->get_expr(), m) << " != ";
              tout << mk_ll_pp(r2->get_expr(), m) << "\n";
              );

        DEBUG_CODE(
            push_trail(push_back_trail<enode_pair, false>(m_diseq_vector));
            m_diseq_vector.push_back(enode_pair(n1, n2)););

        if (r1 == r2) {
            TRACE(add_diseq_inconsistent, tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
            //return false;

            theory_id  t1 = r1->m_th_var_list.get_id();
            if (t1 == null_theory_id) return false;
            return get_theory(t1)->use_diseqs();
        }

        // Propagate disequalities to theories
        if (r1->m_th_var_list.get_next() == nullptr && r2->m_th_var_list.get_next() == nullptr) {
            // common case: r2 and r1 have at most one theory var.
            theory_id  t1 = r1->m_th_var_list.get_id();
            theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_var();
            theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t1) : r2->m_th_var_list.get_var();
            TRACE(add_diseq, tout << "one theory diseq\n";
                  tout << v1 << " != " << v2 << "\n";
                  tout << "th1: " << t1 << " th2: " << r2->m_th_var_list.get_id() << "\n";
                  );
            if (t1 != null_theory_id && v1 != null_theory_var && v2 != null_theory_var &&
                t1 == r2->m_th_var_list.get_id()) {
                if (get_theory(t1)->use_diseqs())
                    push_new_th_diseq(t1, v1, v2);
            }
        }
        else {
            theory_var_list * l1 = r1->get_th_var_list();
            while (l1) {
                theory_id  t1 = l1->get_id();
                theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : l1->get_var();
                theory * th   = get_theory(t1);
                TRACE(add_diseq, tout << m.get_family_name(t1) << "\n";);
                if (th->use_diseqs()) {
                    theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t1) : r2->get_th_var(t1);
                    if (v2 != null_theory_var)
                        push_new_th_diseq(t1, v1, v2);
                }
                l1 = l1->get_next();
            }
        }
        return true;
    }

    /**
       \brief Return true if n1 and n2 are known to be disequal in the logical
       context.
    */
    bool context::is_diseq(enode * n1, enode * n2) const {
        SASSERT(n1->get_sort() == n2->get_sort());
        if (m.are_distinct(n1->get_root()->get_expr(), n2->get_root()->get_expr()))
            return true;
        context * _this = const_cast<context*>(this);
        if (!m_is_diseq_tmp) {
            app * eq       = m.mk_eq(n1->get_expr(), n2->get_expr());
            m.inc_ref(eq);
            _this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq);
        }
        else if (m_is_diseq_tmp->get_expr()->get_arg(0)->get_sort() != n1->get_sort()) {
            m.dec_ref(m_is_diseq_tmp->get_expr());
            app * eq = m.mk_eq(n1->get_expr(), n2->get_expr());
            m.inc_ref(eq);
            m_is_diseq_tmp->m_func_decl_id = UINT_MAX;
            m_is_diseq_tmp->m_owner = eq;
        }
        m_is_diseq_tmp->m_args[0] = n1;
        m_is_diseq_tmp->m_args[1] = n2;
        SASSERT(m_is_diseq_tmp->get_num_args() == 2);
        enode * r = m_cg_table.find(m_is_diseq_tmp);
        SASSERT((r != 0) == m_cg_table.contains(m_is_diseq_tmp));
        TRACE(is_diseq, tout << "r: " << r << "\n";);
        if (r) {
            SASSERT(r->is_eq());
            literal l = enode2literal(r->get_root());
            // SASSERT(result == is_diseq_slow(n1, n2));
            return l != true_literal && (l == false_literal || (is_relevant(l) && get_assignment(l) == l_false));
        }
        CTRACE(is_diseq_bug, is_diseq_slow(n1, n2), tout << "#" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
        return false;
    }

    /**
       \brief Slow version of is_diseq
    */
    bool context::is_diseq_slow(enode * n1, enode * n2) const {
        if (n1->get_num_parents() > n2->get_num_parents())
            std::swap(n1, n2);
        for (enode * parent : enode::parents(n1)) {
            if (parent->is_eq() && is_relevant(parent->get_expr()) && get_assignment(enode2bool_var(parent)) == l_false &&
                ((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) ||
                 (parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) {
                TRACE(is_diseq_bug, tout << "parent: #" << parent->get_owner_id() << ", parent->root: #" <<
                      parent->get_root()->get_owner_id() << " assignment(parent): " << get_assignment(enode2bool_var(parent)) <<
                      " args: #" << parent->get_arg(0)->get_owner_id() << " #" << parent->get_arg(1)->get_owner_id() << "\n";);
                return true;
            }
        }
        return false;
    }

#define SMALL_NUM_PARENTS 3

    bool context::is_ext_diseq(enode * n1, enode * n2, unsigned depth) {
        enode * r1 = n1->get_root();
        enode * r2 = n2->get_root();
        if (r1 == r2)
            return false;
        if (r1->is_interpreted() && r2->is_interpreted())
            return true;
        if (is_diseq(n1, n2))
            return true;
        if (r1->get_num_parents() > r2->get_num_parents()) {
            std::swap(n1, n2);
            std::swap(r1, r2);
        }
        if (depth == 0)
            return false;
        if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
            TRACE(is_ext_diseq, tout << enode_pp(n1, *this) << " " << enode_pp(n2, *this) << " " << depth << "\n";);
            for (enode * p1 : enode::parents(r1)) {
                if (!is_relevant(p1))
                    continue;
                if (p1->is_eq())
                    continue;
                if (!p1->is_cgr())
                    continue;
                func_decl * f     = p1->get_decl();
                TRACE(is_ext_diseq, tout << "p1: " << enode_pp(p1, *this) << "\n";);
                unsigned num_args = p1->get_num_args();
                for (enode * p2 : enode::parents(r2)) {
                    if (!is_relevant(p2))
                        continue;
                    if (p2->is_eq())
                        continue;
                    if (!p2->is_cgr())
                        continue;
                    TRACE(is_ext_diseq, tout << "p2: " << enode_pp(p2, *this) << "\n";);
                    if (p1->get_root() != p2->get_root() && p2->get_decl() == f && p2->get_num_args() == num_args) {
                        unsigned j = 0;
                        for (j = 0; j < num_args; j++) {
                            enode * arg1 = p1->get_arg(j)->get_root();
                            enode * arg2 = p2->get_arg(j)->get_root();
                            if (arg1 == arg2)
                                continue;
                            if ((arg1 == r1 || arg1 == r2) &&
                                (arg2 == r1 || arg2 == r2))
                                continue;
                            break;
                        }
                        if (j == num_args) {
                            TRACE(is_ext_diseq, tout << "found parents: " << enode_pp(p1, *this) << " " << enode_pp(p2, *this) << "\n";);
                            if (is_ext_diseq(p1, p2, depth - 1))
                                return true;
                        }
                    }
                }
            }
        }
        else {
            if (depth >= m_almost_cg_tables.size()) {
                unsigned old_sz = m_almost_cg_tables.size();
                m_almost_cg_tables.resize(depth+1);
                for (unsigned i = old_sz; i < depth + 1; i++)
                    m_almost_cg_tables[i] = alloc(almost_cg_table);
            }
            almost_cg_table & table = *(m_almost_cg_tables[depth]);
            table.reset(r1, r2);
            for (enode * p1 : enode::parents(r1)) {
                if (!is_relevant(p1))
                    continue;
                if (p1->is_eq())
                    continue;
                if (!p1->is_cgr())
                    continue;
                table.insert(p1);
            }
            if (table.empty())
                return false;
            for (enode * p2 : enode::parents(r2)) {
                if (!is_relevant(p2))
                    continue;
                if (p2->is_eq())
                    continue;
                if (!p2->is_cgr())
                    continue;
                list<enode*> * ps = table.find(p2);
                while (ps) {
                    enode * p1 = ps->head();
                    if (p1->get_root() != p2->get_root() && is_ext_diseq(p1, p2, depth - 1))
                        return true;
                    ps = ps->tail();
                }
            }
        }
        return false;
    }

    /**
       \brief Return an enode n congruent to (f args). If there is no such enode in the E-graph, then return 0.
     */
    enode * context::get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) {
        enode * tmp = m_tmp_enode.set(f, num_args, args);
        enode * r   = m_cg_table.find(tmp);
#ifdef Z3DEBUG
        if (r != nullptr) {
            SASSERT(r->get_expr()->get_decl() == f);
            SASSERT(r->get_num_args() == num_args);
            if (r->is_commutative()) {
                // TODO
            }
            else {
                for (unsigned i = 0; i < num_args; i++) {
                    expr * arg   = r->get_expr()->get_arg(i);
                    SASSERT(e_internalized(arg));
                    enode * _arg = get_enode(arg);
                    CTRACE(eq_to_bug, args[i]->get_root() != _arg->get_root(),
                           tout << "#" << args[i]->get_expr_id() << " #" << args[i]->get_root()->get_expr_id()
                           << " #" << _arg->get_expr_id() << " #" << _arg->get_root()->get_expr_id() << "\n";
                           tout << "#" << r->get_expr_id() << "\n";
                           display(tout););
                    SASSERT(args[i]->get_root() == _arg->get_root());
                }
            }
        }
#endif
        return r;
    }

    /**
       \brief Process the equality propagation queue.

       \remark The method assign_eq adds a new entry on this queue.
    */
    bool context::propagate_eqs() {
        unsigned i = 0;
        for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
            new_eq & entry = m_eq_propagation_queue[i];
            add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
            if (inconsistent()) {
                m_eq_propagation_queue.reset();
                return false;
            }
        }
        m_eq_propagation_queue.reset();
        return true;
    }

    /**
       \brief Process equalities, theory atoms, etc.
    */
    bool context::propagate_atoms() {
        SASSERT(!inconsistent());
        CTRACE(propagate_atoms, !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";);
        for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) {
            SASSERT(!inconsistent());
            literal  l = m_atom_propagation_queue[i];
            bool_var v = l.var();
            lbool val  = get_assignment(v);
            TRACE(propagate_atoms, tout << "propagating atom, #" << bool_var2expr(v)->get_id() 
                  << ", is_enode(): " << get_bdata(v).is_enode() << " tag: " 
                  << (get_bdata(v).is_eq()?"eq":"") 
                  << (get_bdata(v).is_theory_atom()?"th":"") 
                  << (get_bdata(v).is_quantifier()?"q":"") << " " << l << "\n";);
            SASSERT(val != l_undef);
            if (get_bdata(v).is_enode())
                propagate_bool_var_enode(v);
            if (inconsistent())
                return false;
            bool_var_data & d = get_bdata(v);
            if (d.is_eq()) {
                app * n = to_app(m_bool_var2expr[v]);
                SASSERT(m.is_eq(n));
                expr * lhs = n->get_arg(0);
                expr * rhs = n->get_arg(1);
                if (m.is_bool(lhs)) {
                    // no-op
                }
                else if (val == l_true) {
                    add_eq(get_enode(lhs), get_enode(rhs), eq_justification(l));
                }
                else {
                    TRACE(add_diseq, display_eq_detail(tout, bool_var2enode(v)););
                    if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) {
                        literal n_eq = literal(l.var(), true);
                        set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), n_eq);
                    }
                }
            }
            else if (d.is_theory_atom()) {
                theory * th = m_theories.get_plugin(d.get_theory());
                SASSERT(th);
                th->assign_eh(v, val == l_true);                
            }
            else if (d.is_quantifier()) {
                // Remark: when RELEVANCY_LEMMA is true, a quantifier can be asserted to false and marked as relevant.
                // This happens when a quantifier is part of a lemma (conflict-clause), and this conflict clause
                // becomes an unit-clause and the remaining literal is the negation of a quantifier.
                CTRACE(assign_quantifier_bug, get_assignment(v) != l_true,
                       tout << "#" << bool_var2expr(v)->get_id() << " val: " << get_assignment(v) << "\n";
                       tout << mk_pp(bool_var2expr(v), m) << "\n";
                       display(tout););
                SASSERT(is_quantifier(m_bool_var2expr[v]));
                if (get_assignment(v) == l_true) {
                    // All universal quantifiers have positive polarity in the input formula.
                    // So, we can ignore quantifiers assigned to false.
                    assign_quantifier(to_quantifier(m_bool_var2expr[v]));
                }
            }
            if (inconsistent())
                return false;
        }
        m_atom_propagation_queue.reset();
        return true;
    }

    class set_var_theory_trail : public trail {
        context& ctx;
        bool_var m_var;
    public:
        set_var_theory_trail(context& ctx, bool_var v): ctx(ctx), m_var(v) {}
        void undo() override {
            bool_var_data & d = ctx.m_bdata[m_var];
            d.reset_notify_theory();
        }
    };

    void context::set_var_theory(bool_var v, theory_id tid) {
        SASSERT(get_var_theory(v) == null_theory_var);
        SASSERT(tid > 0 && tid <= 255);
        SASSERT(get_intern_level(v) <= m_scope_lvl);
        if (m_scope_lvl > get_intern_level(v))
            push_trail(set_var_theory_trail(*this, v));
        bool_var_data & d = m_bdata[v];
        d.set_notify_theory(tid);
    }

    /**
       \brief Propagate the truth value assigned to v, to the enode
       associated with v.  Let n be the enode associated with v. Then,
       this method merges n = true_term (n = false_term) if v was
       assigned to true (false).
    */
    void context::propagate_bool_var_enode(bool_var v) {
        SASSERT(get_assignment(v) != l_undef);
        SASSERT(get_bdata(v).is_enode());
        lbool val  = get_assignment(v);
        TRACE(propagate_bool_var_enode_bug, tout << "var: " << v << " #" << bool_var2expr(v)->get_id() << "\n";);
        SASSERT(v < m_b_internalized_stack.size());
        enode * n  = bool_var2enode(v);

        CTRACE(mk_bool_var, !n, tout << "No enode for " << v << "\n";);
        bool sign  = val == l_false;
        if (n->merge_tf())
            add_eq(n, sign ? m_false_enode : m_true_enode, eq_justification(literal(v, sign)));
        if (watches_fixed(n)) 
            assign_fixed(n, sign ? m.mk_false() : m.mk_true(), literal(v, sign));
        enode * r = n->get_root();
        if (r == m_true_enode || r == m_false_enode)
            return;
        // Move truth value to other elements of the equivalence class if:
        //   1) n is the root of the equivalence class
        //   2) n is not the root, but the variable associated with the root is unassigned.
        if (n == r ||
            !is_relevant(r) || // <<<< added to fix propagation bug.
            get_assignment(enode2bool_var(r)) != val) {
            enode * first = n;
            n = n->get_next();
            while (n != first) {
                bool_var v2 = enode2bool_var(n);
                if (get_assignment(v2) != val)
                    assign(literal(v2, sign), mk_justification(mp_iff_justification(first, n)));
                n = n->get_next();
            }
        }
    }

    /**
       \brief Traverse the disequalities of r's equivalence class, and
       propagate them to the theory.
    */
    void context::push_new_th_diseqs(enode * r, theory_var v, theory * th) {
        if (!th->use_diseqs()) {
            TRACE(push_new_th_diseqs, tout << m.get_family_name(th->get_id()) << " not using diseqs\n";);
            return;
        }
        theory_id th_id = th->get_id();
        TRACE(push_new_th_diseqs, tout << "#" << r->get_owner_id() << " " << mk_bounded_pp(r->get_expr(), m) << " v" << v << " th: " << th_id << "\n";);
        for (enode * parent : r->get_parents()) {
            CTRACE(parent_bug, parent == 0, tout << "#" << r->get_owner_id() << ", num_parents: " << r->get_num_parents() << "\n"; display(tout););
            if (parent->is_eq()) {
                bool_var bv = get_bool_var_of_id(parent->get_owner_id());
                if (get_assignment(bv) == l_false) {
                    enode * lhs = parent->get_arg(0);
                    enode * rhs = parent->get_arg(1);
                    TRACE(push_new_th_diseqs,
                          tout << "#" << parent->get_owner_id() << " ";
                           tout << "lhs: #" << lhs->get_owner_id() << ", rhs: #" << rhs->get_owner_id() <<
                           ", lhs->root: #" << lhs->get_root()->get_owner_id() << ", rhs->root: #" << rhs->get_root()->get_owner_id() <<
                           ", r: #" << r->get_owner_id() << ", r->root: #" << r->get_root()->get_owner_id() << "\n";
                          );
                    CTRACE(push_new_th_diseqs, lhs->get_root() != r->get_root() && rhs->get_root() != r->get_root(),
                           tout << "lhs: #" << lhs->get_owner_id() << ", rhs: #" << rhs->get_owner_id() <<
                           ", lhs->root: #" << lhs->get_root()->get_owner_id() << ", rhs->root: #" << rhs->get_root()->get_owner_id() <<
                           ", r: #" << r->get_owner_id() << ", r->root: #" << r->get_root()->get_owner_id() << "\n";
                          display(tout););
                    SASSERT(lhs->get_root() == r->get_root() || rhs->get_root() == r->get_root());
                    if (rhs->get_root() == r->get_root())
                        std::swap(lhs, rhs);
                    enode * rhs_root   = rhs->get_root();
                    theory_var rhs_var = m_fparams.m_new_core2th_eq ? get_closest_var(rhs, th_id) : rhs_root->get_th_var(th_id);
                    if (m_fparams.m_new_core2th_eq) {
                        theory_var _v = get_closest_var(lhs, th_id);
                        if (_v != null_theory_var)
                            v = _v;
                    }
                    if (rhs_var != null_theory_var && v != rhs_var /* if v == rhs_var then the context will detect the inconsistency. */)
                        push_new_th_diseq(th_id, v, rhs_var);
                }
            }
        }
    }

    /**
       \brief Return the truth assignment for an expression
       that is attached to a boolean variable.

       \pre The expression must be attached to a boolean variable.
    */
    inline lbool context::get_assignment_core(expr * n) const {
        CTRACE(get_assignment_bug, !b_internalized(n), tout << "n:\n" << mk_pp(n, m) << "\n"; display(tout););
        SASSERT(b_internalized(n));
        unsigned id  = n->get_id();
        bool_var var = get_bool_var_of_id(id);
        SASSERT(var != null_bool_var);
        return get_assignment(var);
    }

    /**
       \brief Return the truth assignment for an expression.
       If the expression is a not-application, then its child
       is inspected instead.
    */
    lbool context::get_assignment(expr * n) const {
        if (m.is_false(n))
            return l_false;
        expr* arg = nullptr;
        if (m.is_not(n, arg))
            return ~get_assignment_core(arg);
        return get_assignment_core(n);
    }

    lbool context::find_assignment(expr * n) const {
        if (m.is_false(n))
            return l_false;
        expr* arg = nullptr;
        if (m.is_not(n, arg)) {
            if (b_internalized(arg))
                return ~get_assignment_core(arg);
            return l_undef;
        }
        if (b_internalized(n))
            return get_assignment(n);
        return l_undef;
    }

    /**
       \brief Return the assignment of a 'boolean' enode.
       If the enode is not boolean, then return l_undef.
    */
    lbool context::get_assignment(enode * n) const {
        expr * owner = n->get_expr();
        if (!m.is_bool(owner))
            return l_undef;
        if (n == m_false_enode)
            return l_false;
        bool_var v = get_bool_var_of_id(owner->get_id());
        CTRACE(missing_propagation, v == null_bool_var, tout << mk_pp(owner, m) << "\n";);
        return get_assignment(v);
    }

    /**
       \brief Return set of assigned literals as expressions.
    */
    void context::get_assignments(expr_ref_vector& assignments) {
        for (literal lit : m_assigned_literals) {
            expr_ref e(m);
            literal2expr(lit, e);
            assignments.push_back(std::move(e));
        }
    }

    void context::get_specrels(func_decl_set& rels) const {
        family_id fid = m.get_family_id("specrels");
        theory* th = get_theory(fid);
        if (th)
            static_cast<theory_special_relations*>(th)->get_specrels(rels);
    }


    void context::relevant_eh(expr * n) {
        if (b_internalized(n)) {
            bool_var v        = get_bool_var(n);
            bool_var_data & d = get_bdata(v);
            SASSERT(relevancy());
            // Quantifiers are only asserted when marked as relevant.
            // Other atoms are only asserted when marked as relevant if relevancy_lvl >= 2
            if (d.is_atom() && (d.is_quantifier() || relevancy_lvl() >= 2)) {
                lbool val  = get_assignment(v);
                if (val != l_undef)
                    m_atom_propagation_queue.push_back(literal(v, val == l_false));
            }
        }
        TRACE(propagate_relevancy, tout << "marking as relevant:\n" << mk_bounded_pp(n, m) << " " << m_scope_lvl << "\n";);
        m_case_split_queue->relevant_eh(n);

        if (is_app(n)) {
            if (e_internalized(n)) {
                SASSERT(relevancy());
                enode * e = get_enode(n);
                m_qmanager->relevant_eh(e);
            }

            theory * propagated_th = nullptr;
            family_id fid = to_app(n)->get_family_id();
            if (fid != m.get_basic_family_id()) {
                theory * th = get_theory(fid);
                if (th != nullptr) {
                    th->relevant_eh(to_app(n));
                    propagated_th = th; // <<< mark that relevancy_eh was already invoked for theory th.
                }
            }

            if (e_internalized(n)) {
                enode *           e = get_enode(n);
                theory_var_list * l = e->get_th_var_list();
                while (l) {
                    theory_id  th_id = l->get_id();
                    theory *   th    = get_theory(th_id);
                    // I don't want to invoke relevant_eh twice for the same n.
                    if (th != propagated_th)
                        th->relevant_eh(to_app(n));
                    l = l->get_next();
                }
            }
        }
    }

    /**
       \brief Propagate relevancy using the queue of new assigned literals
       located at [qhead, m_assigned_literals.size()).
    */
    void context::propagate_relevancy(unsigned qhead) {
        if (!relevancy())
            return;
        unsigned sz = m_assigned_literals.size();
        while (qhead < sz) {
            literal l      = m_assigned_literals[qhead];
            SASSERT(get_assignment(l) == l_true);
            qhead++;
            bool_var var   = l.var();
            expr * n       = m_bool_var2expr[var];
            m_relevancy_propagator->assign_eh(n, !l.sign());
        }
        m_relevancy_propagator->propagate();
    }

    bool context::propagate_theories() {
        for (theory * t : m_theory_set) {
            t->propagate();
            if (inconsistent())
                return false;
        }
#if 0
        if (at_search_level() && induction::should_try(*this)) {
            get_induction()();
        }
#endif
        return true;
    }

    void context::propagate_th_eqs() {
        for (unsigned i = 0; i < m_th_eq_propagation_queue.size() && !inconsistent(); i++) {
            new_th_eq curr = m_th_eq_propagation_queue[i];
            theory * th = get_theory(curr.m_th_id);
            SASSERT(th);
            th->new_eq_eh(curr.m_lhs, curr.m_rhs);
            DEBUG_CODE(
                push_trail(push_back_trail<new_th_eq, false>(m_propagated_th_eqs));
                m_propagated_th_eqs.push_back(curr););
        }
        m_th_eq_propagation_queue.reset();
    }

    void context::propagate_th_diseqs() {
        for (unsigned i = 0; i < m_th_diseq_propagation_queue.size() && !inconsistent(); i++) {
            new_th_eq curr = m_th_diseq_propagation_queue[i];
            theory * th = get_theory(curr.m_th_id);
            SASSERT(th);
            th->new_diseq_eh(curr.m_lhs, curr.m_rhs);
            DEBUG_CODE(
                push_trail(push_back_trail<new_th_eq, false>(m_propagated_th_diseqs));
                m_propagated_th_diseqs.push_back(curr););
        }
        m_th_diseq_propagation_queue.reset();
    }

    bool context::can_theories_propagate() const {
        return any_of(m_theory_set, [&](theory* t) { return t->can_propagate(); });
    }

    bool context::can_propagate() const {
        return
            m_qhead != m_assigned_literals.size() ||
            m_relevancy_propagator->can_propagate() ||
            !m_atom_propagation_queue.empty() ||
            m_qmanager->can_propagate() ||
            can_theories_propagate() ||
            !m_eq_propagation_queue.empty() ||
            !m_th_eq_propagation_queue.empty() ||
            !m_th_diseq_propagation_queue.empty();
    }

    /**
       \brief unit propagation.
       Cancelation is not safe during propagation at base level because
       congruences cannot be retracted to a consistent state.
     */
    bool context::propagate() {
        TRACE(propagate, tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n");
        
        while (true) {
            if (inconsistent())
                return false;
            unsigned qhead = m_qhead;
            {
                scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level());
                if (!bcp())
                    return false;
                if (!propagate_th_case_split(qhead))
                    return false;
                SASSERT(!inconsistent());
                propagate_relevancy(qhead);
                if (inconsistent())
                    return false;
                if (!propagate_atoms())
                    return false;
                if (!propagate_eqs())
                    return false;
                propagate_th_eqs();
                propagate_th_diseqs();
                if (inconsistent())
                    return false;
                if (!propagate_theories())
                    return false;
            }
            if (!get_cancel_flag()) {
//                scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level());
                m_qmanager->propagate();
            }
            if (inconsistent())
                return false;
            if (resource_limits_exceeded()) {
                m_qhead = qhead;
                return true;
            }
            if (!can_propagate()) {
                CASSERT("diseq_bug", inconsistent() || check_missing_diseq_conflict());
                CASSERT("eqc_bool", check_eqc_bool_assignment());
                return true;
            }
        }
    }

    void context::set_conflict(const b_justification & js, literal not_l) {
        if (!inconsistent()) {
            TRACE(set_conflict, display_literal_verbose(tout << m_scope_lvl << " ", not_l); display(tout << " ", js); );
            m_conflict = js;
            m_not_l    = not_l;
        }
    }

    void context::assign_quantifier(quantifier * q) {
        TRACE(assumption, tout << mk_pp(q, m) << "\n";);
        m_qmanager->assign_eh(q);
    }

    bool context::contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings) {
        return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings);
    }

    bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
                               unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
        return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
    }

    void context::rescale_bool_var_activity() {
        TRACE(case_split, tout << "rescale\n";);        
        svector<double>::iterator it  = m_activity.begin();
        svector<double>::iterator end = m_activity.end();
        for (; it != end; ++it)
            *it *= INV_ACTIVITY_LIMIT;
        m_bvar_inc *= INV_ACTIVITY_LIMIT;
    }

    /**
       \brief Returns a truth value for the given variable
    */
    bool context::guess(bool_var var, lbool phase) {
        if (is_quantifier(m_bool_var2expr[var])) {
            // Overriding any decision on how to assign the quantifier.
            // assigning a quantifier to false is equivalent to make it irrelevant.
            phase = l_false;
        }
        literal l(var, false);

        if (phase != l_undef)
            return phase == l_true;

        bool_var_data & d = m_bdata[var];
        if (d.try_true_first())
            return true;
        switch (m_fparams.m_phase_selection) {
        case PS_THEORY:
            if (m_phase_cache_on && d.m_phase_available) {
                return m_bdata[var].m_phase;
            }
            if (!m_phase_cache_on && d.is_theory_atom()) {
                theory * th = m_theories.get_plugin(d.get_theory());
                lbool th_phase = th->get_phase(var);
                if (th_phase != l_undef) {
                    return th_phase == l_true;
                }
            }
            if (track_occs()) {
                if (m_lit_occs[l.index()] == 0) {
                    return false;
                }
                if (m_lit_occs[(~l).index()] == 0) {
                    return true;
                }
            }
            return m_phase_default;
        case PS_CACHING:
        case PS_CACHING_CONSERVATIVE:
        case PS_CACHING_CONSERVATIVE2:
            if (m_phase_cache_on && d.m_phase_available) {
                TRACE(phase_selection, tout << "using cached value, is_pos: " << m_bdata[var].m_phase << ", var: p" << var << "\n";);
                return m_bdata[var].m_phase;
            }
            else {
                TRACE(phase_selection, tout << "setting to false\n";);
                return m_phase_default;
            }
        case PS_ALWAYS_FALSE:
            return false;
        case PS_ALWAYS_TRUE:
            return true;
        case PS_RANDOM:
            return m_random() % 2 == 0;
        case PS_OCCURRENCE: {
            return m_lit_occs[l.index()] > m_lit_occs[(~l).index()];
        }
        default:
            UNREACHABLE();
            return false;
        }
    }

    /**
       \brief Execute next case split, return false if there are no
       more case splits to be performed.
    */
    bool context::decide() {

        if (at_search_level() && !m_tmp_clauses.empty()) {
            switch (decide_clause()) {
            case l_true:  // already satisfied
                break;
            case l_undef: // made a decision
                return true;
            case l_false: // inconsistent
                return false;
            }
        }
        bool_var var;
        bool is_pos;
        bool used_queue = false;
        
        if (!has_split_candidate(var, is_pos)) {
            lbool phase = l_undef;
            m_case_split_queue->next_case_split(var, phase);
            used_queue = true;
            if (var == null_bool_var) {
                push_trail(value_trail(m_has_case_split, false));
                return false;
            }

            TRACE_CODE({
                static unsigned counter = 0;
                counter++;
                if (counter % 100 == 0) {
                    TRACE(activity_profile,
                          for (unsigned i=0; i<get_num_bool_vars(); i++) {
                              tout << get_activity(i) << " ";
                          }
                          tout << "\n";);
                }});
        
            is_pos = guess(var, phase);
        }

        m_stats.m_num_decisions++;

        push_scope();
        TRACE(decide, tout << "splitting, lvl: " << m_scope_lvl << "\n";);

        TRACE(decide_detail, tout << mk_pp(bool_var2expr(var), m) << "\n";);
        
        literal l(var, false);

        bool_var original_choice = var;

        if (decide_user_interference(var, is_pos)) {
            if (used_queue)
                m_case_split_queue->unassign_var_eh(original_choice);
            l = literal(var, false);
        }

        if (!is_pos) l.neg();
        TRACE(decide, tout << "case split " << l << "\n" << "activity: " << get_activity(var) << "\n";);
        assign(l, b_justification::mk_axiom(), true);
        return true;
    }
    
    /**
       \brief Update counter that is used to enable/disable phase caching.
    */
    void context::update_phase_cache_counter() {
        m_phase_counter++;
        if (m_phase_cache_on) {
            if (m_phase_counter >= m_fparams.m_phase_caching_on) {
                m_phase_counter  = 0;
                m_phase_cache_on = false;
                if (m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE2)
                    m_phase_default = !m_phase_default;
            }
        }
        else {
            if (m_phase_counter >= m_fparams.m_phase_caching_off) {
                m_phase_counter  = 0;
                m_phase_cache_on = true;
                if (m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE2)
                    m_phase_default = !m_phase_default;
            }
        }
    }

    /**
       \brief Create an internal backtracking point
    */
    void context::push_scope() {

        if (m.has_trace_stream() && !m_is_auxiliary)
            m.trace_stream() << "[push] " << m_scope_lvl << "\n";

        m_scope_lvl++;
        m_region.push_scope();
        m_scopes.push_back(scope());
        scope & s = m_scopes.back();
        // TRACE(context, tout << "push " << m_scope_lvl << "\n";);

        m_relevancy_propagator->push();
        s.m_assigned_literals_lim    = m_assigned_literals.size();
        s.m_trail_stack_lim          = m_trail_stack.size();
        s.m_aux_clauses_lim          = m_aux_clauses.size();
        s.m_justifications_lim       = m_justifications.size();
        s.m_units_to_reassert_lim    = m_units_to_reassert.size();

        m_qmanager->push();

        m_fingerprints.push_scope();
        m_case_split_queue->push_scope();
        m_asserted_formulas.push_scope();

        for (theory* t : m_theory_set) 
            t->push_scope_eh();
        CASSERT("context", check_invariant());
    }

    /**
       \brief Execute generic undo-objects.
    */
    void context::undo_trail_stack(unsigned old_size) {
        ::undo_trail_stack(m_trail_stack, old_size);
    }

    /**
       \brief Remove watch literal idx from the given clause.

       \pre idx must be 0 or 1.
    */
    void context::remove_watch_literal(clause * cls, unsigned idx) {
        m_watches[(~cls->get_literal(idx)).index()].remove_clause(cls);
    }

    /**
       \brief Remove boolean variable from watch lists.
    */
    void context::remove_watch(bool_var v) {
        literal lit(v);
        m_watches[lit.index()].reset();
        m_watches[(~lit).index()].reset();
    }

    /**
       \brief Remove clause
    */

    void context::remove_cls_occs(clause * cls) {
        remove_watch_literal(cls, 0);
        remove_watch_literal(cls, 1);
        remove_lit_occs(*cls, get_num_bool_vars());
    }

    /**
       \brief Update occurrence count of literals
    */

    void context::add_lit_occs(clause const& cls) {
        if (!track_occs()) return;
        for (literal l : cls) {
            inc_ref(l);
        }
    }

    void context::remove_lit_occs(clause const& cls, unsigned nbv) {
        if (!track_occs()) return;
        for (literal l : cls) {
            if (l.var() < nbv) 
                dec_ref(l);
        }
    }

    // TBD: enable as assertion when ready to re-check
    void context::dec_ref(literal l) { if (track_occs() && m_lit_occs[l.index()] > 0) m_lit_occs[l.index()]--; }

    void context::inc_ref(literal l) { if (track_occs()) m_lit_occs[l.index()]++; }

    /**
       \brief Delete the given clause.

       \pre Clause is not in the reinit stack.
    */
    void context::del_clause(bool log, clause * cls) {
        SASSERT(m_flushing || !cls->in_reinit_stack());
        if (log) 
            m_clause_proof.del(*cls);
        CTRACE(context, !m_flushing, display_clause_smt2(tout << "deleting ", *cls) << "\n";);
        if (!cls->deleted())
            remove_cls_occs(cls);
        cls->deallocate(m);
        m_stats.m_num_del_clause++;
    }

    /**
       \brief Delete the clauses in v at locations [old_size .. v.size())
       Reduce the size of v to old_size.
    */
    void context::del_clauses(clause_vector & v, unsigned old_size) {
        unsigned num_collect = v.size() - old_size;
        if (num_collect == 0)
            return;
        
        clause_vector::iterator begin = v.begin() + old_size;
        clause_vector::iterator it    = v.end();
        if (num_collect > 1000) {
            uint_set watches;
            while (it != begin) {
                --it;
                clause* c = *it;
                remove_lit_occs(*c, get_num_bool_vars());
                if (!c->deleted()) {
                    c->mark_as_deleted(m);                    
                }
                watches.insert((~c->get_literal(0)).index());
                watches.insert((~c->get_literal(1)).index());
            }
            for (auto w: watches) {
                m_watches[w].remove_deleted();
            }
            for (it = v.end(); it != begin; ) {
                --it;
                (*it)->deallocate(m);
            }
            m_stats.m_num_del_clause += (v.size() - old_size);
        }
        else {
            while (it != begin) {
                --it;
                del_clause(false, *it);
            }
        }
        v.shrink(old_size);
    }


    /**
       \brief Undo variable assignments.
    */
    void context::unassign_vars(unsigned old_lim) {
        SASSERT(old_lim <= m_assigned_literals.size());

        unsigned i = m_assigned_literals.size();
        while (i != old_lim) {
            --i;
            literal l                  = m_assigned_literals[i];
            CTRACE(assign_core, l.var() == 13, tout << "unassign " << l << "\n";);
            m_assignment[l.index()]    = l_undef;
            m_assignment[(~l).index()] = l_undef;
            bool_var v                 = l.var();
            bool_var_data & d          = get_bdata(v);
            d.set_null_justification();
            m_case_split_queue->unassign_var_eh(v);
        }

        m_assigned_literals.shrink(old_lim);
        m_qhead = old_lim;
        SASSERT(m_qhead == m_assigned_literals.size());
    }

    /**
       \brief Invoke method del_eh for the justification that will be deleted.
       If the method in_region() returns false, then delete operator is invoked.
    */
    void context::del_justifications(ptr_vector<justification> & justifications, unsigned old_lim) {
        SASSERT(old_lim <= justifications.size());
        unsigned i = justifications.size();
        while (i != old_lim) {
            --i;
            justification * js = justifications[i];
            js->del_eh(m);
            if (!js->in_region()) {
                dealloc(js);
            }
            else {
                // If the justification is in a region, then explicitly invoke the destructor.
                // This is needed because some justification objects contains vectors.
                // The destructors of these vectors need to be invoked.
                js->~justification();
            }
        }
        justifications.shrink(old_lim);
    }

    /**
       \brief Return true if all literals of c are assigned to false.
    */
    bool context::is_empty_clause(clause const * c) const {
        unsigned num_lits = c->get_num_literals();
        for(unsigned i = 0; i < num_lits; i++) {
            literal l = c->get_literal(i);
            if (get_assignment(l) != l_false)
                return false;
        }
        return true;
    }

    /**
       \brief Return true if the given clause contains one and only one unassigned literal.
    */
    bool context::is_unit_clause(clause const * c) const {
        bool found        = false;
        unsigned num_lits = c->get_num_literals();
        for(unsigned i = 0; i < num_lits; i++) {
            literal l = c->get_literal(i);
            switch (get_assignment(l)) {
            case l_false:
                break; // skip
            case l_undef:
                if (found)
                    return false;
                else
                    found = true;
                break;
            case l_true:
                return false; // clause is already satisfied.
            }
        }
        return found;
    }

    /**
       \brief When a clause is reinitialized (see reinit_clauses) enodes and literals may
       need to be recreated. When an enode is recreated, I want to use the same generation
       number it had before being deleted. Otherwise the generation will be 0, and will affect
       the loop prevention heuristics used to control quantifier instantiation.
       Thus, I cache the generation number of enodes that will be deleted during backtracking
       and recreated by reinit_clauses.
    */
    void context::cache_generation(unsigned new_scope_lvl) {
        if (!m_clauses_to_reinit.empty()) {
            unsigned lim = m_scope_lvl;
            if (m_clauses_to_reinit.size() <= lim) {
                SASSERT(!m_clauses_to_reinit.empty());
                lim      = m_clauses_to_reinit.size() - 1;
            }
            for (unsigned i = new_scope_lvl; i <= lim; i++) {
                clause_vector & v = m_clauses_to_reinit[i];
                for (clause* cls : v) {
                    cache_generation(cls, new_scope_lvl);
                }
            }
        }
        if (!m_units_to_reassert.empty()) {
            scope & s   = m_scopes[new_scope_lvl];
            unsigned i  = s.m_units_to_reassert_lim;
            unsigned sz = m_units_to_reassert.size();
            for (; i < sz; i++) {
                expr* unit = m_units_to_reassert[i].m_unit.get();
                cache_generation(unit, new_scope_lvl);
            }
        }
    }

    /**
       \brief See cache_generation(unsigned new_scope_lvl)
    */
    void context::cache_generation(clause const * cls, unsigned new_scope_lvl) {
        cache_generation(cls->get_num_literals(), cls->begin(), new_scope_lvl);
    }

    /**
       \brief See cache_generation(unsigned new_scope_lvl)
    */
    void context::cache_generation(unsigned num_lits, literal const * lits, unsigned new_scope_lvl) {
        for(unsigned i = 0; i < num_lits; i++) {
            bool_var v          = lits[i].var();
            unsigned ilvl       = get_intern_level(v);
            if (ilvl > new_scope_lvl)
                cache_generation(bool_var2expr(v), new_scope_lvl);
        }
    }

    /**
       \brief See cache_generation(unsigned new_scope_lvl)
    */
    void context::cache_generation(expr * n, unsigned new_scope_lvl) {
        ptr_buffer<expr> todo;
        todo.push_back(n);
        while (!todo.empty()) {
            expr * n = todo.back();
            todo.pop_back();
            if (m_cache_generation_visited.contains(n))
                continue;
            m_cache_generation_visited.insert(n);
            if (is_app(n)) {
                if (e_internalized(n)) {
                    enode * e     = get_enode(n);
                    unsigned ilvl = e->get_iscope_lvl();
                    if (ilvl <= new_scope_lvl)
                        continue; // node and its children will not be recreated during backtracking
                    TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";);
                    m_cached_generation.insert(n, e->get_generation());
                }
                for (expr * arg : *to_app(n)) {
                    if (is_app(arg) || is_quantifier(arg))
                        todo.push_back(arg);
                }
            }
            else if (is_quantifier(n) && b_internalized(n)) {
                m_cached_generation.insert(n, m_qmanager->get_generation(to_quantifier(n)));
                todo.push_back(to_quantifier(n)->get_expr());
            }
        }
    }

    /**
       \brief See cache_generation(unsigned new_scope_lvl)
    */
    void context::reset_cache_generation() {
        m_cache_generation_visited.reset();
        m_cached_generation.reset();
    }

    /**
       \brief Reinitialize learned clauses (lemmas) that contain boolean variables
       that were deleted during backtracking.

       \remark num_bool_vars contains the number of boolean variables alive
       after backtracking. So, a clause contains a dead variable if it
       contains a literal l where l.var() >= num_bool_vars.
    */
    void context::reinit_clauses(unsigned num_scopes, unsigned num_bool_vars) {
        if (m_clauses_to_reinit.empty())
            return;
        unsigned lim = m_scope_lvl + num_scopes;
        if (m_clauses_to_reinit.size() <= lim) {
            SASSERT(!m_clauses_to_reinit.empty());
            lim      = m_clauses_to_reinit.size() - 1;
        }
        for (unsigned i = m_scope_lvl+1; i <= lim; i++) {
            clause_vector & v = m_clauses_to_reinit[i];
            for (clause* cls : v) {
                if (cls->deleted()) {
                    cls->release_atoms(m);
                    cls->m_reinit              = false;
                    cls->m_reinternalize_atoms = false;
                    continue;
                }
                SASSERT(cls->in_reinit_stack());
                bool keep = false;
                if (cls->reinternalize_atoms()) {
                    SASSERT(cls->get_num_atoms() == cls->get_num_literals());
                    for (unsigned j = 0; j < 2; j++) {
                        literal l           = cls->get_literal(j);
                        if (l.var() < num_bool_vars) {
                            // This boolean variable was not deleted during backtracking
                            //
                            // So, it is still a watch literal. I remove the watch, since
                            // the clause may have new watch-literals after reinitialization.
                            remove_watch_literal(cls, j);
                        }
                    }

                    unsigned num = cls->get_num_literals();

                    remove_lit_occs(*cls, num_bool_vars);

                    unsigned ilvl       = 0;
                    (void)ilvl;
                    for (unsigned j = 0; j < num; j++) {
                        expr * atom     = cls->get_atom(j);
                        bool   sign     = cls->get_atom_sign(j);
                        // Atom can be (NOT foo). This can happen, for example, when
                        // the NOT-application is a child of an uninterpreted function symbol.
                        // So, when reinternalizing the NOT-atom I should set the gate_ctx to false,
                        // and force expression to be reinternalized.
                        // Otherwise I set gate_ctx to true
                        bool gate_ctx = !m.is_not(atom);
                        internalize(atom, gate_ctx);
                        SASSERT(b_internalized(atom));
                        bool_var v      = get_bool_var(atom);
                        DEBUG_CODE({
                            if (get_intern_level(v) > ilvl)
                                ilvl = get_intern_level(v);
                        });
                        literal l(v, sign);
                        cls->set_literal(j, l);
                        if (cls->get_kind() == CLS_TH_LEMMA)
                            mark_as_relevant(l);
                    }
                    SASSERT(ilvl <= m_scope_lvl);
                    int w1_idx = select_watch_lit(cls, 0);
                    cls->swap_lits(0, w1_idx);
                    int w2_idx = select_watch_lit(cls, 1);
                    cls->swap_lits(1, w2_idx);
                    add_watch_literal(cls, 0);
                    add_watch_literal(cls, 1);

                    add_lit_occs(*cls);

                    literal l1 = cls->get_literal(0);
                    literal l2 = cls->get_literal(1);

                    if (get_assignment(l1) == l_false)
                        set_conflict(b_justification(cls));
                    else if (get_assignment(l2) == l_false)
                        assign(l1, b_justification(cls));

                    TRACE(reinit_clauses, tout << "reinit clause:\n"; display_clause_detail(tout, cls); tout << "\n";
                          tout << "activity: " << cls->get_activity() << ", num_bool_vars: " << num_bool_vars << ", scope_lvl: "
                          << m_scope_lvl << "\n";);
                    keep = true;
                }
                else {
                    SASSERT(!cls->reinternalize_atoms());
                    literal l1 = cls->get_literal(0);
                    literal l2 = cls->get_literal(1);
                    if (cls->get_kind() == CLS_TH_LEMMA) {
                        mark_as_relevant(l1);
                        mark_as_relevant(l2);
                    }
                    if (get_assignment(l1) == l_false && is_empty_clause(cls)) {
                        set_conflict(b_justification(cls));
                        keep = true;
                    }
                    else if (get_assignment(l2) == l_false && get_assignment(l1) == l_undef && is_unit_clause(cls)) {
                        assign(l1, b_justification(cls));
                        keep = true;
                    }
                }

                if (keep && m_scope_lvl > m_base_lvl) {
                    m_clauses_to_reinit[m_scope_lvl].push_back(cls);
                }
                else {
                    // clause do not need to be in the reinit stack anymore,
                    // because it will be deleted when the base level is
                    // backtracked.
                    cls->release_atoms(m);
                    cls->m_reinit              = false;
                    cls->m_reinternalize_atoms = false;
                }
            }
            v.reset();
        }
        CASSERT("reinit_clauses", check_clauses(m_lemmas));
        TRACE(reinit_clauses_bug, display_watch_lists(tout););
    }

    void context::reassert_units(unsigned units_to_reassert_lim) {
        unsigned i  = units_to_reassert_lim;
        unsigned sz = m_units_to_reassert.size();
        for (; i < sz; i++) {
            auto [unit, sign, is_relevant] = m_units_to_reassert[i];
            bool gate_ctx = true;
            internalize(unit, gate_ctx);
            bool_var v    = get_bool_var(unit);
            literal l(v, sign);
            assign(l, b_justification::mk_axiom());
            if (is_relevant)
                mark_as_relevant(l);
            TRACE(reassert_units, tout << "reasserting #" << unit->get_id() << " " << sign << " @ " << m_scope_lvl << "\n";);            
        }
        if (at_base_level()) 
            m_units_to_reassert.reset();        
    }

    /**
       \brief Backtrack 'num_scopes' scope levels. Return the number
       of boolean variables before reinitializing clauses. This value
       is useful because it can be used to detect which boolean variables
       were deleted.

       \warning This method will not invoke reset_cache_generation.
    */
    unsigned context::pop_scope_core(unsigned num_scopes) {
        unsigned units_to_reassert_lim;

        try {
            if (m.has_trace_stream() && !m_is_auxiliary)
                m.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";

            // TRACE(context, tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
            TRACE(pop_scope_detail, display(tout););
            SASSERT(num_scopes > 0);
            SASSERT(num_scopes <= m_scope_lvl);
            SASSERT(m_scopes.size() == m_scope_lvl);

            unsigned new_lvl = m_scope_lvl - num_scopes;

            cache_generation(new_lvl);
            m_qmanager->pop(num_scopes);
            m_case_split_queue->pop_scope(num_scopes);

            TRACE(pop_scope, tout << "backtracking: " << num_scopes << ", new_lvl: " << new_lvl << "\n";);
            scope & s = m_scopes[new_lvl];
            TRACE(context, tout << "backtracking new_lvl: " << new_lvl << "\n";);

            units_to_reassert_lim = s.m_units_to_reassert_lim;

            if (new_lvl < m_base_lvl) {
                base_scope & bs = m_base_scopes[new_lvl];
                del_clauses(m_lemmas, bs.m_lemmas_lim);
                m_simp_qhead = bs.m_simp_qhead_lim;
                if (!bs.m_inconsistent) {
                    m_conflict = null_b_justification;
                    m_not_l = null_literal;
                    m_unsat_proof = nullptr;
                }
                m_base_scopes.shrink(new_lvl);
            }
            else {
                m_conflict = null_b_justification;
                m_not_l = null_literal;
            }
            del_clauses(m_aux_clauses, s.m_aux_clauses_lim);

            m_relevancy_propagator->pop(num_scopes);

            m_fingerprints.pop_scope(num_scopes);
            unassign_vars(s.m_assigned_literals_lim);
            undo_trail_stack(s.m_trail_stack_lim);

            for (theory* th : m_theory_set) 
                th->pop_scope_eh(num_scopes);

            del_justifications(m_justifications, s.m_justifications_lim);

            m_asserted_formulas.pop_scope(num_scopes);

            CTRACE(propagate_atoms, !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";);

            m_eq_propagation_queue.reset();
            m_th_eq_propagation_queue.reset();
            m_th_diseq_propagation_queue.reset();
            m_atom_propagation_queue.reset();
            m_region.pop_scope(num_scopes);
            m_scopes.shrink(new_lvl);
            m_conflict_resolution->reset();

            m_scope_lvl = new_lvl;
            if (new_lvl < m_base_lvl) {
                m_base_lvl = new_lvl;
                m_search_lvl = new_lvl; // Remark: not really necessary
            }
        }
        catch (...) {
            // throwing inside pop is just not cool.
            UNREACHABLE();
        }

        // an exception can happen when axioms are reinitialized (because they are rewritten).

        unsigned num_bool_vars = get_num_bool_vars();
        // any variable >= num_bool_vars was deleted during backtracking.
        reinit_clauses(num_scopes, num_bool_vars);
        reassert_units(units_to_reassert_lim);
        TRACE(pop_scope_detail, tout << "end of pop_scope: \n"; display(tout););
        CASSERT("context", check_invariant());
        return num_bool_vars;
    }

    void context::pop_scope(unsigned num_scopes) {
        pop_scope_core(num_scopes);
        reset_cache_generation();
    }

    void context::pop_to_base_lvl() {
        SASSERT(m_scope_lvl >= m_base_lvl);
        if (!at_base_level()) {
            unsigned num_lvls = m_scope_lvl - m_base_lvl;
            pop_scope(num_lvls);
        }
        SASSERT(m_scope_lvl == m_base_lvl);
    }

    void context::pop_to_search_lvl() {
        if (m_scope_lvl > get_search_level()) {
            pop_scope(m_scope_lvl - get_search_level());
        }
    }

    /**
       \brief Simplify the given clause using the assignment.  Return
       true if the clause was already satisfied, and false otherwise.

       \remark This method should only be invoked if we are at the
       base level.
    */
    bool context::simplify_clause(clause& cls) {
        SASSERT(m_scope_lvl == m_base_lvl);
        unsigned s = cls.get_num_literals();
        if (get_assignment(cls[0]) == l_true ||
            get_assignment(cls[1]) == l_true) {
            // clause is already satisfied.
            return true;
        }

        literal_buffer simp_lits;

        unsigned i = 2;
        unsigned j = i;
        bool is_taut = false;
        for(; i < s; i++) {
            literal l = cls[i];
            switch(get_assignment(l)) {
            case l_false:
                if (m.proofs_enabled())
                    simp_lits.push_back(~l);
                dec_ref(l);
                break;
            case l_true:
                is_taut = true;
                // fallthrough
            case l_undef:
                if (i != j) {
                    cls.swap_lits(i, j);
                }
                j++;
                break;
            }
        }

        if (j < s) {
            m_clause_proof.shrink(cls, j);
            cls.set_num_literals(j);
            SASSERT(j >= 2);
        }

        if (is_taut) {
            return true;
        }

        if (m.proofs_enabled() && !simp_lits.empty()) {
            SASSERT(m_scope_lvl == m_base_lvl);
            justification * js = cls.get_justification();
            justification * new_js = nullptr;
            if (js->in_region())
                new_js = mk_justification(unit_resolution_justification(*this,
                                                                        js,
                                                                        simp_lits.size(),
                                                                        simp_lits.data()));
            else
                new_js = alloc(unit_resolution_justification, js, simp_lits.size(), simp_lits.data());
            cls.set_justification(new_js);
        }
        return false;
    }

    /**
       \brief Simplify the given vector of clauses starting at the given position.
       Return the number of deleted (already satisfied) clauses.
    */
    unsigned context::simplify_clauses(clause_vector & clauses, unsigned starting_at) {
        unsigned num_del_clauses = 0;
        clause_vector::iterator it  = clauses.begin();
        clause_vector::iterator end = clauses.end();
        it += starting_at;
        clause_vector::iterator it2 = it;
        for(; it != end; ++it) {
            clause * cls = *it;
            SASSERT(!cls->in_reinit_stack());
            
            if (cls->deleted()) {
                TRACE(simplify_clauses_bug, display_clause(tout << "deleted\n", cls) << "\n";);
                del_clause(true, cls);
                num_del_clauses++;
            }
            else if (simplify_clause(*cls)) {
                TRACE(simplify_clauses_bug, display_clause_smt2(tout << "simplified\n", *cls) << "\n";);
                for (unsigned idx = 0; idx < 2; idx++) {
                    literal     l0        = (*cls)[idx];
                    b_justification l0_js = get_justification(l0.var());
                    if (l0_js != null_b_justification &&
                        l0_js.get_kind() == b_justification::CLAUSE &&
                        l0_js.get_clause() == cls) {
                        // cls is the explanation of l0
                        // it is safe to replace with axiom, we are at the base level.
                        SASSERT(m_scope_lvl == m_base_lvl);
                        bool_var v0 = l0.var();
                        if (m.proofs_enabled()) {
                            SASSERT(m_search_lvl == m_base_lvl);
                            literal_buffer simp_lits;
                            unsigned num_lits = cls->get_num_literals();
                            for(unsigned i = 0; i < num_lits; i++) {
                                if (i != idx) {
                                    literal l = (*cls)[i];
                                    SASSERT(l != l0);
                                    simp_lits.push_back(~l);
                                }
                            }
                            justification * cls_js = cls->get_justification();
                            justification * js = nullptr;
                            if (!cls_js || cls_js->in_region()) {
                                // If cls_js is 0 or is allocated in a region, then
                                // we can allocate the new justification in a region too.
                                js = mk_justification(unit_resolution_justification(*this,
                                                                                    cls_js,
                                                                                    simp_lits.size(),
                                                                                    simp_lits.data()));
                            }
                            else {
                                js = alloc(unit_resolution_justification, cls_js, simp_lits.size(), simp_lits.data());
                                // js took ownership of the justification object.
                                cls->set_justification(nullptr);
                                m_justifications.push_back(js);
                            }
                            set_justification(v0, m_bdata[v0], b_justification(js));
                        }
                        else
                            m_bdata[v0].set_axiom();
                    }
                }
                del_clause(true, cls);
                num_del_clauses++;
            }
            else {
                *it2 = *it;
                ++it2;
                m_simp_counter += cls->get_num_literals();
            }
        }
        clauses.set_end(it2);
        CASSERT("simplify_clauses", check_invariant());
        return num_del_clauses;
    }

    /**
       \brief Simplify the set of clauses if possible (solver is at base level).
    */
    void context::simplify_clauses() {
        // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed.
        if (m_scope_lvl > m_base_lvl)
            return;

        unsigned sz = m_assigned_literals.size();
        SASSERT(m_simp_qhead <= sz);

        if (m_simp_qhead == sz || m_simp_counter > 0) {
            TRACE(simplify_clauses, tout << "m_simp_qhead: " << m_simp_qhead << " m_simp_counter: " << m_simp_counter << "\n";);
            return;
        }

        if (m_aux_clauses.empty() && m_lemmas.empty()) {
            TRACE(simplify_clauses, tout << "no clauses to simplify\n";);
            return;
        }

        TRACE(simplify_clauses_detail, tout << "before:\n"; display_clauses(tout, m_lemmas););

        SASSERT(check_clauses(m_lemmas));
        SASSERT(check_clauses(m_aux_clauses));


        // m_simp_counter is used to balance the cost of simplify_clause.
        //
        // After executing simplify_clauses, the counter will contain
        // an approximation of the cost of executing simplify_clauses again.
        // That is, the number of literals that will need to be visited.
        //
        // The value of the counter is decremented each time we visit
        // a variable during propagation.
        //
        m_simp_counter = 0;
        // the field m_simp_qhead is used to check whether there are
        // new assigned literals at the base level.
        m_simp_qhead = m_assigned_literals.size();

        unsigned num_del_clauses = 0;

        SASSERT(m_scope_lvl == m_base_lvl);
        if (m_base_lvl == 0) {
            num_del_clauses += simplify_clauses(m_aux_clauses, 0);
            num_del_clauses += simplify_clauses(m_lemmas, 0);
        }
        else {
            scope & s       = m_scopes[m_base_lvl - 1];
            base_scope & bs = m_base_scopes[m_base_lvl - 1];
            num_del_clauses += simplify_clauses(m_aux_clauses, s.m_aux_clauses_lim);
            num_del_clauses += simplify_clauses(m_lemmas, bs.m_lemmas_lim);
        }
        m_stats.m_num_del_clauses += num_del_clauses;
        m_stats.m_num_simplifications++;
        TRACE(simp_counter, tout << "simp_counter: " << m_simp_counter << " scope_lvl: " << m_scope_lvl << "\n";);
        TRACE(simplify_clauses_detail, tout << "after:\n"; display_clauses(tout, m_lemmas););
        SASSERT(check_clauses(m_lemmas) && check_clauses(m_aux_clauses));
    }

    struct clause_lt {
        bool operator()(clause * cls1, clause * cls2) const { return cls1->get_activity() > cls2->get_activity(); }
    };

    /**
       \brief Delete low activity lemmas
    */
    inline void context::del_inactive_lemmas() {
        if (m_fparams.m_lemma_gc_strategy == LGC_NONE)
            return;
        else if (m_fparams.m_lemma_gc_half)
            del_inactive_lemmas1();
        else
            del_inactive_lemmas2();

        m_num_conflicts_since_lemma_gc = 0;
        if (m_fparams.m_lemma_gc_strategy == LGC_GEOMETRIC)
            m_lemma_gc_threshold = static_cast<unsigned>(m_lemma_gc_threshold * m_fparams.m_lemma_gc_factor);
    }

    /**
       \brief Delete (approx.) half of low activity lemmas
    */
    void context::del_inactive_lemmas1() {
        unsigned sz            = m_lemmas.size();
        unsigned start_at      = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim;
        SASSERT(start_at <= sz);
        if (start_at + m_fparams.m_recent_lemmas_size >= sz)
            return;
        IF_VERBOSE(2, verbose_stream() << "(smt.delete-inactive-lemmas"; verbose_stream().flush(););
        SASSERT (m_fparams.m_recent_lemmas_size < sz);
        unsigned end_at        = sz - m_fparams.m_recent_lemmas_size;
        SASSERT(start_at < end_at);
        std::stable_sort(m_lemmas.begin() + start_at, m_lemmas.begin() + end_at, clause_lt());
        unsigned start_del_at  = (start_at + end_at) / 2;
        unsigned i             = start_del_at;
        unsigned j             = i;
        unsigned num_del_cls   = 0;
        TRACE(del_inactive_lemmas, tout << "sz: " << sz << ", start_at: " << start_at << ", end_at: " << end_at
              << ", start_del_at: " << start_del_at << "\n";);
        for (; i < end_at; i++) {
            clause * cls = m_lemmas[i];
            if (can_delete(cls)) {
                TRACE(del_inactive_lemmas, tout << "deleting: "; display_clause(tout, cls); tout << ", activity: " <<
                      cls->get_activity() << "\n";);
                del_clause(true, cls);
                num_del_cls++;
            }
            else {
                m_lemmas[j] = cls;
                j++;
            }
        }
        // keep recent clauses
        for (; i < sz; i++) {
            clause * cls = m_lemmas[i];
            if (cls->deleted() && can_delete(cls)) {
                del_clause(true, cls);
                num_del_cls++;
            }
            else {
                m_lemmas[j++] = cls;
            }
        }
        m_lemmas.shrink(j);
        if (m_fparams.m_clause_decay > 1) {
            // rescale activity
            for (i = start_at; i < j; i++) {
                clause * cls = m_lemmas[i];
                cls->set_activity(cls->get_activity() / m_fparams.m_clause_decay);
            }
        }
        IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_cls << ")" << std::endl;);
    }

    /**
       \brief More sophisticated version of del_inactive_lemmas. Here the lemmas are divided in two
       groups (old and new) based on the value of m_new_old_ratio parameter.
       A clause is deleted/retained based on its activity and relevancy. Clauses with several
       unassigned literals are considered less relevant. The threshold used for activity and relevancy
       depends on which group the clauses is in.
    */
    void context::del_inactive_lemmas2() {
        IF_VERBOSE(2, verbose_stream() << "(smt.delete-inactive-clauses "; verbose_stream().flush(););
        unsigned sz            = m_lemmas.size();
        unsigned start_at      = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim;
        SASSERT(start_at <= sz);
        unsigned real_sz       = sz - start_at;
        // idx of the first learned clause considered "new"
        unsigned new_first_idx = start_at + (real_sz / m_fparams.m_new_old_ratio) * (m_fparams.m_new_old_ratio - 1);
        SASSERT(new_first_idx <= sz);
        unsigned i             = start_at;
        unsigned j             = i;
        unsigned num_del_cls   = 0;
        for (; i < sz; i++) {
            clause * cls = m_lemmas[i];
            if (can_delete(cls)) {
                if (cls->deleted()) {
                    // clause is already marked for deletion
                    del_clause(true, cls);
                    num_del_cls++;
                    continue;
                }
                // A clause is deleted if it has low activity and the number of unknowns is greater than a threshold.
                // The activity threshold depends on how old the clause is.
                unsigned act_threshold = m_fparams.m_old_clause_activity -
                    (m_fparams.m_old_clause_activity - m_fparams.m_new_clause_activity) * ((i - start_at) / real_sz);
                if (cls->get_activity() < act_threshold) {
                    unsigned rel_threshold = (i >= new_first_idx ? m_fparams.m_new_clause_relevancy : m_fparams.m_old_clause_relevancy);
                    if (more_than_k_unassigned_literals(cls, rel_threshold)) {
                        del_clause(true, cls);
                        num_del_cls++;
                        continue;
                    }
                }
            }
            m_lemmas[j] = cls;
            j++;
            cls->set_activity(static_cast<unsigned>(cls->get_activity() / m_fparams.m_inv_clause_decay));
        }
        SASSERT(j <= sz);
        m_lemmas.shrink(j);
        IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_cls << ")" << std::endl;);
    }

    /**
       \brief Return true if "cls" has more than (or equal to) k unassigned literals.
    */
    bool context::more_than_k_unassigned_literals(clause * cls, unsigned k) {
        SASSERT(k > 0);
        for (literal l : *cls) {
            if (get_assignment(l) == l_undef) {
                k--;
                if (k == 0) {
                    return true;
                }
            }
        }
        return false;
    }


#ifdef Z3DEBUG
    /**
       \brief Return true if a symbol of the given theory was already internalized.
    */
    bool context::already_internalized_theory(theory * th) const {
        return already_internalized_theory_core(th, m_b_internalized_stack) || already_internalized_theory_core(th, m_e_internalized_stack);
    }

    /**
       \brief Auxiliary method for #already_internalized_theory.
    */
    bool context::already_internalized_theory_core(theory * th, expr_ref_vector const & s) const {        
        expr_mark visited;
        family_id fid = th->get_id();
        unsigned sz = s.size();
        for (unsigned i = 0; i < sz; i++) {
            expr * n = s.get(i);
            if (uses_theory(n, fid, visited)) {
                return true;
            }
        }
        return false;
    }
#endif

    void context::register_plugin(theory * th) {
        if (m_theories.get_plugin(th->get_family_id()) != nullptr) {
            dealloc(th);
            return; // context already has a theory for the given family id.
        }
        TRACE(internalize, tout << this << " " << th->get_family_id() << "\n";);
        SASSERT(std::find(m_theory_set.begin(), m_theory_set.end(), th) == m_theory_set.end());
        m_theories.register_plugin(th);
        th->init();
        m_theory_set.push_back(th);
        {
#ifdef Z3DEBUG
            // It is unsafe to invoke push_trail from the method push_scope_eh.
            flet<bool> l(m_trail_enabled, false);
#endif
            for (unsigned i = 0; i < m_scope_lvl; ++i)
                th->push_scope_eh();
        }
    }

    void context::user_propagate_init(
        void*                    ctx, 
        user_propagator::push_eh_t&       push_eh,
        user_propagator::pop_eh_t&        pop_eh,
        user_propagator::fresh_eh_t&      fresh_eh) {
        setup_context(false);
        m_user_propagator = alloc(theory_user_propagator, *this);
        m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
        for (unsigned i = m_scopes.size(); i-- > 0; ) 
            m_user_propagator->push_scope_eh();
        register_plugin(m_user_propagator);
    }

    void context::user_propagate_initialize_value(expr* var, expr* value) {
        m_values.push_back({expr_ref(var, m), expr_ref(value, m)});
        push_trail(push_back_vector(m_values));
    }

    void context::initialize_value(expr* var, expr* value) {
        IF_VERBOSE(10, verbose_stream() << "initialize " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
        sort* s = var->get_sort();
        ensure_internalized(var);
            
        if (m.is_bool(s)) {
            auto v = get_bool_var_of_id_option(var->get_id());
            if (v == null_bool_var) {
                IF_VERBOSE(5, verbose_stream() << "Boolean variable has no literal " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
                return;
            }
            m_bdata[v].m_phase_available = true;         
            if (m.is_true(value))
                m_bdata[v].m_phase = true;
            else if (m.is_false(value))
                m_bdata[v].m_phase = false;
            else
                IF_VERBOSE(5, verbose_stream() << "Boolean value is not constant " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
            return;                
        }

        if (!e_internalized(var))
            return;
        theory* th = m_theories.get_plugin(s->get_family_id());
        if (!th) {
            IF_VERBOSE(5, verbose_stream() << "No theory is attached to variable " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
            return;
        }
        th->initialize_value(var, value);

    }

    bool context::watches_fixed(enode* n) const {
        return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get_family_id()) != null_theory_var;
    }

    bool context::has_split_candidate(bool_var& var, bool& is_pos) {
        if (!m_user_propagator)
            return false;
        if (!m_user_propagator->get_case_split(var, is_pos))
            return false;
        return get_assignment(var) == l_undef;
    }
    
    bool context::decide_user_interference(bool_var& var, bool& is_pos) {
        if (!m_user_propagator)
            return false;
        bool_var old = var;
        m_user_propagator->decide(var, is_pos);
        return old != var;
    }

    void context::assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain) {
        theory_var v = n->get_th_var(m_user_propagator->get_family_id());
        m_user_propagator->new_fixed_eh(v, val, sz, explain);
    }

    bool context::is_fixed(enode* n, expr_ref& val, literal_vector& explain) {
        if (m.is_bool(n->get_expr())) {
            literal lit = get_literal(n->get_expr());
            switch (get_assignment(lit)) {
            case l_true:
                val = m.mk_true(); explain.push_back(lit); return true;
            case l_false:
                val = m.mk_false(); explain.push_back(~lit); return true;
            default:
                return false;
            }
        }
        theory_var_list * l = n->get_th_var_list();
        while (l) {
            theory_id tid = l->get_id();
            auto* p = m_theories.get_plugin(tid);
            if (p && p->is_fixed_propagated(l->get_var(), val, explain))
                return true;
            l = l->get_next();
        }
        return false;
    }


    void context::push() {       
        pop_to_base_lvl();
        setup_context(false);
        bool was_consistent = !inconsistent();
        try {
            internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
        } catch (oom_exception&) {
            throw default_exception("Resource limits hit in push");
        }
        if (!m.inc())
            throw default_exception("push canceled");
        scoped_suspend_rlimit _suspend_cancel(m.limit());
        propagate();
        if (was_consistent && inconsistent() && !m_asserted_formulas.inconsistent()) {
            // logical context became inconsistent during user PUSH
            VERIFY(!resolve_conflict()); // build the proof
        }
        push_scope();
        m_base_scopes.push_back(base_scope());
        base_scope & bs = m_base_scopes.back();
        bs.m_lemmas_lim = m_lemmas.size();
        bs.m_inconsistent = inconsistent();
        bs.m_simp_qhead_lim = m_simp_qhead;
        m_base_lvl++;
        m_search_lvl++; // Not really necessary. But, it is useful to enforce the invariant m_search_lvl >= m_base_lvl
        SASSERT(m_base_lvl <= m_scope_lvl);
    }

    void context::pop(unsigned num_scopes) {
        SASSERT (num_scopes > 0);
        if (num_scopes > m_scope_lvl) return;
        pop_to_base_lvl();
        pop_scope(num_scopes);
    }

    /**
       \brief Free memory allocated by logical context.
    */
    void context::flush() {
        flet<bool> l1(m_flushing, true);
        TRACE(flush, tout << "m_scope_lvl: " << m_scope_lvl << "\n";);
        m_relevancy_propagator = nullptr;
        m_model_generator->reset();
        for (theory* t : m_theory_set) {
            t->flush_eh();
        }
        del_clauses(m_aux_clauses, 0);
        del_clauses(m_lemmas, 0);
        del_justifications(m_justifications, 0);
        reset_tmp_clauses();
        undo_trail_stack(0);
        m_qmanager = nullptr;
        if (m_is_diseq_tmp) {
            m_is_diseq_tmp->del_eh(m, false);
            m.dec_ref(m_is_diseq_tmp->get_expr());
            enode::del_dummy(m_is_diseq_tmp);
            m_is_diseq_tmp = nullptr;
        }
        std::for_each(m_almost_cg_tables.begin(), m_almost_cg_tables.end(), delete_proc<almost_cg_table>());
    }

    void context::assert_expr_core(expr * e, proof * pr) {
        if (get_cancel_flag()) return;
        SASSERT(is_well_sorted(m, e));
        TRACE(begin_assert_expr, tout << mk_pp(e, m) << " " << mk_pp(pr, m) << "\n";);
        TRACE(begin_assert_expr_ll, tout << mk_ll_pp(e, m) << "\n";);
        if (!m_searching)
            pop_to_base_lvl();
        if (pr == nullptr)
            m_asserted_formulas.assert_expr(e);
        else
            m_asserted_formulas.assert_expr(e, pr);
        TRACE(end_assert_expr_ll, ast_mark m; m_asserted_formulas.display_ll(tout, m););
    }

    void context::add_asserted(expr* e) {
        m_asserted_formulas.assert_expr(e);
    }

    void context::assert_expr(expr * e) {
        assert_expr(e, nullptr);
    }

    void context::assert_expr(expr * e, proof * pr) {
        timeit tt(get_verbosity_level() >= 100, "smt.simplifying");
        assert_expr_core(e, pr);
    }

    class case_split_insert_trail : public trail {
        context& ctx;
        literal l;
    public:
        case_split_insert_trail(context& ctx, literal l):
            ctx(ctx),
            l(l) {
        }
        void undo() override {
            ctx.undo_th_case_split(l);
        }
    };

    void context::mk_th_case_split(unsigned num_lits, literal * lits) {
        TRACE(theory_case_split, display_literals_verbose(tout << "theory case split: ", num_lits, lits); tout << std::endl;);
        // If we don't use the theory case split heuristic,
        // for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2)
        // to enforce the condition that at most one literal can be assigned 'true'.
        if (!m_fparams.m_theory_case_split) {
            if (!m.proofs_enabled()) {
                for (unsigned i = 0; i < num_lits; ++i) {
                    for (unsigned j = i + 1; j < num_lits; ++j) {
                        literal l1 = lits[i];
                        literal l2 = lits[j];
                        mk_clause(~l1, ~l2, (justification*) nullptr);
                    }
                }
            }
        }
        else {
            literal_vector new_case_split;
            for (unsigned i = 0; i < num_lits; ++i) {
                literal l = lits[i];
                SASSERT(!m_all_th_case_split_literals.contains(l.index()));
                m_all_th_case_split_literals.insert(l.index());
                push_trail(case_split_insert_trail(*this, l));
                new_case_split.push_back(l);
            }
            m_th_case_split_sets.push_back(new_case_split);
            push_trail(push_back_vector<vector<literal_vector> >(m_th_case_split_sets));
            for (unsigned i = 0; i < num_lits; ++i) {
                literal l = lits[i];
                if (!m_literal2casesplitsets.contains(l.index())) {
                    m_literal2casesplitsets.insert(l.index(), vector<literal_vector>());
                }
                m_literal2casesplitsets[l.index()].push_back(new_case_split);
            }
            TRACE(theory_case_split, tout << "tracking case split literal set { ";
                  for (unsigned i = 0; i < num_lits; ++i) {
                      tout << lits[i].index() << " ";
                  }
                  tout << "}" << std::endl;
                  );
        }
    }

    void context::add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
        m_case_split_queue->add_theory_aware_branching_info(v, priority, phase);
    }

    void context::undo_th_case_split(literal l) {
        m_all_th_case_split_literals.remove(l.index());
        if (m_literal2casesplitsets.contains(l.index())) {
            if (!m_literal2casesplitsets[l.index()].empty()) {
                m_literal2casesplitsets[l.index()].pop_back();
            }
        }
    }

    bool context::propagate_th_case_split(unsigned qhead) {
        if (m_all_th_case_split_literals.empty())
            return true;

        // iterate over all literals assigned since the last time this method was called,
        // not counting any literals that get assigned by this method
        // this relies on bcp() to give us its old m_qhead and therefore
        // bcp() should always be called before this method

        unsigned assigned_literal_end = m_assigned_literals.size();
        for (; qhead < assigned_literal_end; ++qhead) {
            literal l = m_assigned_literals[qhead];
            TRACE(theory_case_split, tout << "check literal " << l.index() << std::endl; display_literal_verbose(tout, l); tout << std::endl;);
            // check if this literal participates in any theory case split
            if (!m_all_th_case_split_literals.contains(l.index())) {
                continue;
            }
            TRACE(theory_case_split, tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
            // now find the sets of literals which contain l
            vector<literal_vector> const& case_split_sets = m_literal2casesplitsets[l.index()];
            for (const auto& case_split_set : case_split_sets) {
                TRACE(theory_case_split, tout << "found case split set { ";
                      for (const auto& set_elem : case_split_set) {
                          tout << set_elem.index() << " ";
                      }
                      tout << "}" << std::endl;);
                for (const auto& l2 : case_split_set) {
                    if (l2 != l) {
                        b_justification js(l);
                        TRACE(theory_case_split, tout << "case split literal "; smt::display(tout, l2, m, m_bool_var2expr.data()); tout << std::endl;);
                        if (l2 == true_literal || l2 == false_literal || l2 == null_literal) continue;
                        assign(~l2, js);
                        if (inconsistent()) {
                            TRACE(theory_case_split, tout << "conflict detected!" << std::endl;);
                            return false;
                        }
                    }
                }
            }
        }
        // if we get here without detecting a conflict, we're fine
        return true;
    }

    void context::reduce_assertions() {
        if (!m_asserted_formulas.inconsistent()) {
            // SASSERT(at_base_level());
            m_asserted_formulas.reduce();
        }
    }

    static bool is_valid_assumption(ast_manager & m, expr * a) {
        expr* arg;
        if (!m.is_bool(a))
            return false;
        if (is_uninterp_const(a))
            return true;
        if (m.is_not(a, arg) && is_uninterp_const(arg))
            return true;
        if (!is_app(a))
            return false;
        if (m.is_true(a) || m.is_false(a))
            return true;
        if (is_app(a) && to_app(a)->get_family_id() == m.get_basic_family_id())
            return false;
        if (is_app(a) && to_app(a)->get_num_args() == 0)
            return true;
        return false;
    }

    void context::internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy) {
        for (expr* e : asms) {
            if (is_valid_assumption(m, e)) {
                asm2proxy.push_back(std::make_pair(e, expr_ref(e, m)));
            }
            else {
                expr_ref proxy(m), fml(m);
                proxy = m.mk_fresh_const(symbol(), m.mk_bool_sort());
                fml = m.mk_implies(proxy, e);
                m_asserted_formulas.assert_expr(fml);
                asm2proxy.push_back(std::make_pair(e, proxy));
            }
        }
        // The new assertions are of the form 'proxy => assumption'
        // so clause simplification is sound even as these are removed after pop_scope.
        internalize_assertions();
    }

    void context::internalize_assertions() {
        if (get_cancel_flag()) return;
        if (m_internalizing_assertions) return;
        flet<bool> _internalizing(m_internalizing_assertions, true);
        TRACE(internalize_assertions, tout << "internalize_assertions()...\n";);
        timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
        unsigned qhead = 0;
        do {
            reduce_assertions();
            if (get_cancel_flag()) 
                return;
            if (m_asserted_formulas.inconsistent()) {
                if (!inconsistent())
                    asserted_inconsistent();
                break;
            }
            qhead = m_asserted_formulas.get_qhead();
            unsigned sz = m_asserted_formulas.get_num_formulas();
            while (qhead < sz) {
                if (get_cancel_flag()) {
                    m_asserted_formulas.commit(qhead);
                    return;
                }
                expr * f   = m_asserted_formulas.get_formula(qhead);
                proof * pr = m_asserted_formulas.get_formula_proof(qhead);
                SASSERT(!pr || f == m.get_fact(pr));                    
                internalize_assertion(f, pr, 0);
                ++qhead;
            }
            m_asserted_formulas.commit();
        }
        while (qhead < m_asserted_formulas.get_num_formulas());

        TRACE(internalize_assertions, tout << "after internalize_assertions()...\n";
              tout << "inconsistent: " << inconsistent() << "\n";);
        TRACE(after_internalize_assertions, display(tout););
    }

    void context::asserted_inconsistent() {
        proof * pr = m_asserted_formulas.get_inconsistency_proof();
        m_unsat_proof = pr;
        if (!pr) {
            set_conflict(b_justification::mk_axiom());
        }
        else {
            set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
        }
    }

    /**
       \brief Assumptions must be uninterpreted boolean constants (aka propositional variables).
    */
    bool context::validate_assumptions(expr_ref_vector const& asms) {
        for (expr* a : asms) {
            SASSERT(a);
            if (!is_valid_assumption(m, a)) {
                warning_msg("an assumption must be a propositional variable or the negation of one");
                return false;
            }
        }
        return true;
    }

    void context::init_clause(expr_ref_vector const& _clause) {
        literal_vector lits;
        for (expr* lit : _clause) {
            internalize_formula(lit, true);
            mark_as_relevant(lit);
            lits.push_back(get_literal(lit));
        }
        clause* clausep = nullptr;
        if (lits.size() >= 2) {
            justification* js = nullptr;
            if (m.proofs_enabled()) {
                proof * pr = mk_clause_def_axiom(lits.size(), lits.data(), nullptr);
                js = mk_justification(justification_proof_wrapper(*this, pr));
            }
            clausep = clause::mk(m, lits.size(), lits.data(), CLS_AUX, js);
        }
        m_tmp_clauses.push_back(std::make_pair(clausep, lits));
    }

    void context::reset_tmp_clauses() {
        for (auto& p : m_tmp_clauses) {
            if (p.first) del_clause(false, p.first);
        }
        m_tmp_clauses.reset();
    }

    lbool context::decide_clause() {
        if (m_tmp_clauses.empty()) return l_true;
        for (auto & tmp_clause : m_tmp_clauses) {
            literal_vector& lits = tmp_clause.second;
            literal unassigned = null_literal;
            for (literal l : lits) {
                switch (get_assignment(l)) {
                case l_false:
                    break;
                case l_true:
                    goto next_clause;
                default:
                    unassigned = l;
                }         
            }

            if (unassigned != null_literal) {
                shuffle(lits.size(), lits.data(), m_random);
                push_scope();
                assign(unassigned, b_justification::mk_axiom(), true);
                return l_undef;
            }

            if (lits.size() == 1) {
                set_conflict(b_justification(), ~lits[0]);
            }
            else {
                set_conflict(b_justification(tmp_clause.first), null_literal);
            }
            VERIFY(!resolve_conflict());
            return l_false;
        next_clause:
            ;
        }
        return l_true;
    }

    void context::init_assumptions(expr_ref_vector const& asms) {
        reset_assumptions();
        m_literal2assumption.reset();
        m_unsat_core.reset();

        if (!asms.empty()) {
            // We must give a chance to the theories to propagate before we create a new scope...
            propagate();
            // Internal backtracking scopes (created with push_scope()) must only be created when we are
            // in a consistent context.
            if (inconsistent())
                return;
            if (get_cancel_flag())
                return;
            del_inactive_lemmas();
            push_scope();
            vector<std::pair<expr*,expr_ref>> asm2proxy;
            internalize_proxies(asms, asm2proxy);
            for (auto const& p: asm2proxy) {
                if (inconsistent())
                    break;
                expr_ref curr_assumption = p.second;
                expr* orig_assumption = p.first;
                if (m.is_true(curr_assumption)) continue;
                SASSERT(is_valid_assumption(m, curr_assumption));
                proof * pr = m.mk_asserted(curr_assumption);
                internalize_assertion(curr_assumption, pr, 0);
                literal l = get_literal(curr_assumption);
                SASSERT(get_assignment(l) != l_undef);
                SASSERT(l != false_literal || inconsistent());
                if (l == true_literal || l == false_literal) {
                    continue;
                }
                m_literal2assumption.insert(l.index(), orig_assumption);
                m_assumptions.push_back(l);
                get_bdata(l.var()).m_assumption = true;                
                SASSERT(is_relevant(l));
                TRACE(assumptions, tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m) << "\n";);
            }
        }
        m_search_lvl = m_scope_lvl;
        SASSERT(asms.empty() || m_search_lvl > m_base_lvl);
        SASSERT(!asms.empty() || m_search_lvl == m_base_lvl);
        TRACE(after_internalization, display(tout););
    }

    void context::reset_assumptions() {
        TRACE(unsat_core_bug, tout << "reset " << m_assumptions << "\n";);
        for (literal lit : m_assumptions) 
            get_bdata(lit.var()).m_assumption = false;
        m_assumptions.reset();
    }

    bool context::should_research(lbool r) {
        if (r != l_false || m_unsat_core.empty()) { 
            return false;
        }
        for (theory* th : m_theory_set) {
            if (th->should_research(m_unsat_core)) {
                return true;
            }
        }
        return false;
    }

    lbool context::mk_unsat_core(lbool r) {        
        if (r != l_false) return r;
        SASSERT(inconsistent());
        if (!tracking_assumptions()) {
            SASSERT(m_assumptions.empty());
            return l_false;
        }
        uint_set already_found_assumptions;
        literal_vector::const_iterator it  = m_conflict_resolution->begin_unsat_core();
        literal_vector::const_iterator end = m_conflict_resolution->end_unsat_core();
        for (; it != end; ++it) {
            literal l = *it;
            TRACE(unsat_core_bug, tout << "answer literal: " << l << "\n";);
            SASSERT(get_bdata(l.var()).m_assumption);
            if (!m_literal2assumption.contains(l.index())) l.neg();
            SASSERT(m_literal2assumption.contains(l.index()));
            if (!already_found_assumptions.contains(l.index())) {
                already_found_assumptions.insert(l.index());
                expr* orig_assumption = m_literal2assumption[l.index()];
                m_unsat_core.push_back(orig_assumption);
                TRACE(assumptions, tout << l << ": " << mk_pp(orig_assumption, m) << "\n";);
            }
        }
        reset_assumptions();
        pop_to_base_lvl(); // undo the push_scope() performed by init_assumptions
        m_search_lvl = m_base_lvl;
        std::sort(m_unsat_core.data(), m_unsat_core.data() + m_unsat_core.size(), ast_lt_proc());
        TRACE(unsat_core_bug, tout << "unsat core:\n" << m_unsat_core << "\n";);
        validate_unsat_core();
        // theory validation of unsat core
        for (theory* th : m_theory_set) {
            lbool theory_result = th->validate_unsat_core(m_unsat_core);
            if (theory_result == l_undef) {
                return l_undef;
            }
        }
        return l_false;
    }

    /**
       \brief Make some checks before starting the search.
       Return true if succeeded.
    */
    bool context::check_preamble(bool reset_cancel) {
        if (m.has_trace_stream() && !m_is_auxiliary)
            m.trace_stream() << "[begin-check] " << m_scope_lvl << "\n";

        if (memory::above_high_watermark()) {
            m_last_search_failure = MEMOUT;
            return false;
        }
        reset_tmp_clauses();
        m_unsat_core.reset();
        m_stats.m_num_checks++;
        pop_to_base_lvl();      
        m_conflict_resolution->reset();
        return true;
    }

    /**
       \brief Execute some finalization code after performing the search.
    */
    lbool context::check_finalize(lbool r) {
        TRACE(after_search, display(tout << "result: " << r << "\n");
              m_case_split_queue->display(tout << "case splits\n");
              );
        m_search_finalized = true;
        display_profile(verbose_stream());
        if (r == l_true && get_cancel_flag()) 
            r = l_undef;
        if (r == l_undef && m_internal_completed == l_true && has_sls_model()) {
            m_last_search_failure = OK;
            m_conflict = null_b_justification;
            r = l_true;
        }
        m_internal_completed = l_false;
        if (r == l_true && gparams::get_value("model_validate") == "true") {
            recfun::util u(m);
            if (u.get_rec_funs().empty() && m_proto_model) {
                for (theory* t : m_theory_set) {
                    t->validate_model(*m_proto_model);
                }
            }
#if 0
            for (literal lit : m_assigned_literals) {
                if (!is_relevant(lit)) continue;
                expr* v = m_bool_var2expr[lit.var()];
                if (lit.sign() ? m_model->is_true(v) : m_model->is_false(v)) {
                    IF_VERBOSE(10, verbose_stream() 
                               << "invalid assignment " << (lit.sign() ? "true" : "false") 
                               << " to #" << v->get_id() << " := " << mk_bounded_pp(v, m, 3) << "\n");
                }
            }
            for (clause* cls : m_aux_clauses) {
                bool found = false;
                IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "check:\n", *cls) << "\n");                    
                for (literal lit : *cls) {
                    expr* v = m_bool_var2expr[lit.var()];
                    if (lit.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
                        found = true;
                        break;
                    }
                }
                if (!found) {
                    IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "not satisfied:\n", *cls) << "\n");                    
                }
            }
            for (clause* cls : m_lemmas) {
                bool found = false;
                IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "check:\n", *cls) << "\n");                    
                for (literal lit : *cls) {
                    expr* v = m_bool_var2expr[lit.var()];
                    if (lit.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
                        found = true;
                        break;
                    }
                }
                if (!found) {
                    IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "not satisfied:\n", *cls) << "\n");                    
                }
            }

            unsigned l_idx = 0;
            for (watch_list const& wl : m_watches) {
                literal l1 = to_literal(l_idx++);
                literal neg_l1 = ~l1;
                expr* v = m_bool_var2expr[l1.var()];
                if (neg_l1.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
                    continue;
                }
                literal const * it2  = wl.begin_literals();
                literal const * end2 = wl.end_literals();
                for (; it2 != end2; ++it2) {
                    literal l2 = *it2;
                    if (l1.index() >= l2.index()) {
                        continue;
                    }
                    literal lits[2] = { neg_l1, l2 };
                    IF_VERBOSE(10, display_literals_smt2(verbose_stream() << "check: ", 2, lits) << "\n";);
                    v = m_bool_var2expr[l2.var()];
                    if (l2.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
                        continue;
                    }
                    IF_VERBOSE(10, display_literals_smt2(verbose_stream() << "not satisfied: ", 2, lits) << "\n";);
                }
            }
#endif
        }
        return r;
    }

    bool context::has_sls_model() {
        if (!m_fparams.m_sls_enable)
            return false;
        auto tid = m.get_family_id("sls");
        auto p = m_theories.get_plugin(tid);
        if (!p)
            return false;
        m_model = static_cast<theory_sls*>(p)->get_model();
        return m_model.get() != nullptr;
    }

    /**
       \brief Setup the logical context based on the current set of
       asserted formulas and execute the check command.

       \remark A logical context can only be configured at scope level 0,
       and before internalizing any formulas.
    */
    lbool context::setup_and_check(bool reset_cancel) {
        if (!check_preamble(reset_cancel)) return l_undef;
        SASSERT(m_scope_lvl == 0);
        SASSERT(!m_setup.already_configured());
        setup_context(m_fparams.m_auto_config);

        if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
            parallel p(*this);
            expr_ref_vector asms(m);
            return p(asms);
        }

        try {
            internalize_assertions();
        } catch (oom_exception&) {
            return l_undef;
        }
        expr_ref_vector theory_assumptions(m);
        add_theory_assumptions(theory_assumptions);
        if (!theory_assumptions.empty()) {
            TRACE(search, tout << "Adding theory assumptions to context" << std::endl;);
            return check(0, nullptr, reset_cancel);
        }
        else {
            search_completion sc(*this);
            TRACE(before_search, display(tout););
            return check_finalize(search());
        }
    }

    config_mode context::get_config_mode(bool use_static_features) const {
        if (!m_fparams.m_auto_config)
            return CFG_BASIC;
        if (use_static_features)
            return CFG_AUTO;
        return CFG_LOGIC;
    }

    void context::setup_context(bool use_static_features) {
        if (m_setup.already_configured() || inconsistent()) {
            m_relevancy_lvl = std::min(m_fparams.m_relevancy_lvl, m_relevancy_lvl);
            return;
        }
        m_setup(get_config_mode(use_static_features));
        m_relevancy_lvl = m_fparams.m_relevancy_lvl;
        setup_components();
    }

    void context::setup_components() {
        m_asserted_formulas.setup();
        m_random.set_seed(m_fparams.m_random_seed);
        m_dyn_ack_manager.setup();
        m_conflict_resolution->setup();

        if (!relevancy())
            m_fparams.m_relevancy_lemma = false;

        // setup all the theories
        for (theory* th : m_theory_set) 
            th->setup();
    }

    void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
        for (theory* th : m_theory_set) {
            th->add_theory_assumptions(theory_assumptions);
        }
    }

    lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
        if (!check_preamble(reset_cancel)) return l_undef;
        SASSERT(at_base_level());
        setup_context(false);
        search_completion sc(*this);
        if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {            
            expr_ref_vector asms(m, num_assumptions, assumptions);
            parallel p(*this);
            return p(asms);
        }
        lbool r = l_undef;
        do {
            pop_to_base_lvl();
            expr_ref_vector asms(m, num_assumptions, assumptions);
            try {
                internalize_assertions();
                add_theory_assumptions(asms);
                TRACE(unsat_core_bug, tout << asms << '\n';);
                init_assumptions(asms);
            } catch (oom_exception&) {
                return l_undef;
            }
            TRACE(before_search, display(tout););
            r = search();
            r = mk_unsat_core(r);        
        }
        while (should_research(r));
        r = check_finalize(r);
        return r;
    }

    lbool context::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
        if (!check_preamble(true)) return l_undef;
        TRACE(before_search, display(tout););
        setup_context(false);
        lbool r = l_undef;
        search_completion sc(*this);
        do {
            pop_to_base_lvl();
            expr_ref_vector asms(cube);
            try {
                internalize_assertions();
                add_theory_assumptions(asms);
                // introducing proxies: if (!validate_assumptions(asms)) return l_undef;
                for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
                init_assumptions(asms);
            } catch (oom_exception&) {
                return l_undef;
            }
            for (auto const& clause : clauses) init_clause(clause);
            r = search();   
            r = mk_unsat_core(r);             
        }
        while (should_research(r));
        r = check_finalize(r);
        return r;           
    }

    void context::init_search() {
        for (theory* th : m_theory_set) {
            th->init_search_eh();
        }
        m_qmanager->init_search_eh();
        m_incomplete_theories.reset();
        m_num_conflicts                = 0;
        m_num_conflicts_since_restart  = 0;
        m_num_conflicts_since_lemma_gc = 0;
        m_num_restarts                 = 0;
        m_restart_threshold            = m_fparams.m_restart_initial;
        m_restart_outer_threshold      = m_fparams.m_restart_initial;
        m_agility                      = 0.0;
        m_luby_idx                     = 1;
        m_lemma_gc_threshold           = m_fparams.m_lemma_gc_initial;
        m_last_search_failure          = OK;
        m_unsat_proof                  = nullptr;
        m_unsat_core                   .reset();
        m_dyn_ack_manager              .init_search_eh();
        m_final_check_idx              = 0;
        m_phase_default                = false;
        m_case_split_queue             ->init_search_eh();
        m_next_progress_sample         = 0;
        m_internal_completed                = l_undef;
        if (m.has_type_vars() && !m_theories.get_plugin(poly_family_id))
            register_plugin(alloc(theory_polymorphism, *this));
        TRACE(literal_occ, display_literal_num_occs(tout););
    }

    void context::initialize_values() {
        if (m_values.empty())
            return;
        expr_safe_replace sub(m);
        for (auto const &[var, value] : m_values) {
            initialize_value(var, value);
            sub.insert(var, value);
        }        
        for (unsigned v = 0; v < get_num_bool_vars(); ++v) {
            expr_ref var(bool_var2expr(v), m);
            if (!var)
                continue;
            sub(var);
            m_rewriter(var);

            if (m.is_true(var)) {
                m_bdata[v].m_phase_available = true;
                m_bdata[v].m_phase = true;
            }
            else if (m.is_false(var)) {
                m_bdata[v].m_phase_available = true;
                m_bdata[v].m_phase = false;
            } 
        }

        for (clause *cls : m_aux_clauses) {
            literal undef_lit = null_literal;
            bool is_true = false;
            for (auto lit : *cls) {
                auto v = lit.var();
                if (m_bdata[v].m_phase_available) {
                    bool phase = m_bdata[v].m_phase;
                    if (lit.sign() != phase) {
                        is_true = true;
                        break;
                    }
                }
                else {
                    undef_lit = lit;
                }
            }
            if (!is_true && undef_lit != null_literal) {
                auto v = undef_lit.var();
                m_bdata[v].m_phase_available = true;
                m_bdata[v].m_phase = !undef_lit.sign();
            }
        }       
    }

    void context::end_search() {
        m_case_split_queue->end_search_eh();
    }

    void context::inc_limits() {
        if (m_num_conflicts_since_restart >= m_restart_threshold) {
            switch (m_fparams.m_restart_strategy) {
            case RS_GEOMETRIC:
                m_restart_threshold = static_cast<unsigned>(m_restart_threshold * m_fparams.m_restart_factor);
                break;
            case RS_IN_OUT_GEOMETRIC:
                m_restart_threshold = static_cast<unsigned>(m_restart_threshold * m_fparams.m_restart_factor);
                if (m_restart_threshold > m_restart_outer_threshold) {
                    m_restart_threshold = m_fparams.m_restart_initial;
                    m_restart_outer_threshold = static_cast<unsigned>(m_restart_outer_threshold * m_fparams.m_restart_factor);
                }
                break;
            case RS_LUBY:
                m_luby_idx ++;
                m_restart_threshold = static_cast<unsigned>(get_luby(m_luby_idx) * m_fparams.m_restart_initial);
                break;
            case RS_FIXED:
                break;
            case RS_ARITHMETIC:
                m_restart_threshold = static_cast<unsigned>(m_restart_threshold + m_fparams.m_restart_factor);
                break;
            default:
                break;
            }
        }
        m_num_conflicts_since_restart = 0;
    }


    lbool context::search() {
        if (m_asserted_formulas.inconsistent()) {
            asserted_inconsistent();
            return l_false;
        }
        if (inconsistent()) {
            VERIFY(!resolve_conflict());
            return l_false;
        }
        if (get_cancel_flag()) 
            return l_undef;
        
        timeit tt(get_verbosity_level() >= 100, "smt.stats");
        reset_model();
        SASSERT(at_search_level());
        TRACE(search, display(tout); display_enodes_lbls(tout););
        TRACE(search_detail, m_asserted_formulas.display(tout););
        init_search();
        initialize_values();
            
        flet<bool> l(m_searching, true);
        TRACE(after_init_search, display(tout););
        IF_VERBOSE(2, verbose_stream() << "(smt.searching)\n";);
        log_stats();
        TRACE(search_lite, tout << "searching...\n";);
        lbool    status            = l_undef;
        unsigned curr_lvl          = m_scope_lvl;

        while (true) {
            SASSERT(!inconsistent());

            status = bounded_search();
            TRACE(search_bug, tout << "status: " << status << ", inconsistent: " << inconsistent() << "\n";);
            TRACE(assigned_literals_per_lvl, display_num_assigned_literals_per_lvl(tout);
                  tout << ", num_assigned: " << m_assigned_literals.size() << "\n";);

            if (!restart(status, curr_lvl)) {
                break;
            }            
        }

        TRACE(guessed_literals,
              expr_ref_vector guessed_lits(m);
              get_guessed_literals(guessed_lits);
              tout << guessed_lits << "\n";);
        end_search();
        return status;
    }

    bool context::restart(lbool& status, unsigned curr_lvl) {
        SASSERT(status != l_true || !inconsistent());

        reset_model();

        if (m_last_search_failure != OK) 
            return false;
        if (status == l_false) 
            return false;
        if (status == l_true && !m_qmanager->has_quantifiers() && !has_lambda()) 
            return false;
        if (status == l_true && m_qmanager->has_quantifiers()) {
            // possible outcomes   DONE l_true, DONE l_undef, CONTINUE
            mk_proto_model();
            quantifier_manager::check_model_result cmr = quantifier_manager::UNKNOWN;
            if (m_proto_model.get()) {
                cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
            }
            switch (cmr) {
            case quantifier_manager::SAT:
                return false;
            case quantifier_manager::UNKNOWN:
                IF_VERBOSE(2, verbose_stream() << "(smt.giveup quantifiers)\n";);
                // giving up
                m_last_search_failure = QUANTIFIERS;
                status = l_undef;
                return false;
            default:
                break;
            }
        }
        if (status == l_true && has_lambda()) {
            m_last_search_failure = LAMBDAS;
            status = l_undef;
            return false;
        }
        inc_limits();
        if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
            SASSERT(!inconsistent());
            log_stats();
            // execute the restart
            m_stats.m_num_restarts++;
            m_num_restarts++;
            if (m_scope_lvl > curr_lvl) {
                pop_scope(m_scope_lvl - curr_lvl);
                SASSERT(at_search_level());
            }
            for (theory* th : m_theory_set) 
                if (!inconsistent()) 
                    th->restart_eh();

            TRACE(mbqi_bug_detail, tout << "before instantiating quantifiers...\n";);
            if (!inconsistent()) 
                m_qmanager->restart_eh();
            if (inconsistent()) {
                VERIFY(!resolve_conflict());
                status = l_false;
                return false;
            }
            if (m_num_restarts >= m_fparams.m_restart_max) {
                status = l_undef;
                m_last_search_failure = NUM_CONFLICTS;
                return false;
            }
        }
        if (m_fparams.m_simplify_clauses)
            simplify_clauses();
        if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART)
            del_inactive_lemmas();

        status = l_undef;
        return true;
    }

    void context::tick(unsigned & counter) const {
        counter++;
        if (counter > m_fparams.m_tick) {
            IF_VERBOSE(3, verbose_stream() << "(smt.working";
                       verbose_stream() << " :conflicts " << m_num_conflicts;
                       // verbose_stream() << " lemma avg. activity: " << get_lemma_avg_activity();
                       if (m_fparams.m_restart_adaptive)
                       verbose_stream() << " :agility " << m_agility;
                       verbose_stream() << ")" << std::endl; verbose_stream().flush(););
            TRACE(assigned_literals_per_lvl, display_num_assigned_literals_per_lvl(tout); tout << "\n";);
            counter = 0;
        }
    }

    lbool context::bounded_search() {
        unsigned counter = 0;

        TRACE(bounded_search, tout << "starting bounded search...\n";);

        while (true) {
            while (!propagate()) {
                TRACE_CODE({
                    static bool first_propagate = true;
                    if (first_propagate) {
                        first_propagate = false;
                        TRACE(after_first_propagate, display(tout););
                    }
                });

                tick(counter);

                if (!resolve_conflict())
                    return l_false;

                SASSERT(m_scope_lvl >= m_base_lvl);

                if (!inconsistent()) {
                    if (resource_limits_exceeded())
                        return l_undef;

                    if (get_cancel_flag())
                        return l_undef;

                    if (m_num_conflicts_since_restart > m_restart_threshold && m_scope_lvl - m_base_lvl > 2) {
                        TRACE(search_bug, tout << "bounded-search return undef, inconsistent: " << inconsistent() << "\n";);
                        return l_undef; // restart
                    }

                    if (m_num_conflicts > m_fparams.m_max_conflicts) {
                        TRACE(search_bug, tout << "bounded-search return undef, inconsistent: " << inconsistent() << "\n";);
                        m_last_search_failure = NUM_CONFLICTS;
                        return l_undef;
                    }
                }

                if (m_num_conflicts_since_lemma_gc > m_lemma_gc_threshold &&
                    (m_fparams.m_lemma_gc_strategy == LGC_FIXED || m_fparams.m_lemma_gc_strategy == LGC_GEOMETRIC)) {
                    del_inactive_lemmas();
                }

                m_dyn_ack_manager.propagate_eh();
                CASSERT("dyn_ack", check_clauses(m_lemmas) && check_clauses(m_aux_clauses));
            }

            if (resource_limits_exceeded() && !inconsistent()) {
                return l_undef;
            }

            if (get_cancel_flag())
                return l_undef;

            if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses)
                simplify_clauses();

            if (!decide()) {
                if (inconsistent()) 
                    return l_false;
                final_check_status fcs = final_check();
                TRACE(final_check_result, tout << "fcs: " << fcs << " last_search_failure: " << m_last_search_failure << "\n";);
                switch (fcs) {
                case FC_DONE:
                    log_stats();
                    return l_true;
                case FC_CONTINUE:
                    break;
                case FC_GIVEUP:
                    return l_undef;
                }
            }

            if (resource_limits_exceeded() && !inconsistent()) {
                return l_undef;
            }
        }
    }

    bool context::resource_limits_exceeded() {
        if (m_searching) {
            // Some of the flags only make sense to check when searching.
            // For example, the timer is only started in init_search().
            if (m_last_search_failure != OK)
                return true;

            if (get_cancel_flag()) 
                return true;            

            if (m_progress_callback) {
                m_progress_callback->fast_progress_sample();
                if (m_fparams.m_progress_sampling_freq > 0 && m_timer.ms_timeout(m_next_progress_sample + 1)) {
                    m_progress_callback->slow_progress_sample();
                    m_next_progress_sample = (unsigned)(m_timer.get_seconds() * 1000) + m_fparams.m_progress_sampling_freq;
                }
            }
        }

        if (get_cancel_flag()) 
            return true;        

        if (memory::above_high_watermark()) {
            m_last_search_failure = MEMOUT;
            return true;
        }

        return false;
    }

    final_check_status context::final_check() {
        TRACE(final_check, tout << "final_check inconsistent: " << inconsistent() << "\n"; display(tout); display_normalized_enodes(tout););
        CASSERT("relevancy", check_relevancy());
        
        if (m_fparams.m_model_on_final_check) {
            mk_proto_model();
            model_pp(std::cout, *m_proto_model);
            std::cout << "END_OF_MODEL" << std::endl;
        }

        m_stats.m_num_final_checks++;
        TRACE(final_check_stats, tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";);

        final_check_status ok = m_qmanager->final_check_eh(false);
        if (ok != FC_DONE)
            return ok;

        m_incomplete_theories.reset();

        unsigned old_idx          = m_final_check_idx;
        unsigned num_th           = m_theory_set.size();
        unsigned range            = num_th + 1;
        final_check_status result = FC_DONE;
        failure  f                = OK;

        do {
            TRACE(final_check_step, tout << "processing: " << m_final_check_idx << ", result: " << result << "\n";);
            final_check_status ok;
            if (m_final_check_idx < num_th) {
                theory * th = m_theory_set[m_final_check_idx];
                IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"" << th->get_name() << "\")\n";);
                ok = th->final_check_eh();
                TRACE(final_check_step, tout << "final check '" << th->get_name() << " ok: " << ok << " inconsistent " << inconsistent() << "\n";);
                if (get_cancel_flag()) {
                    f = CANCELED;
                    ok = FC_GIVEUP;
                }
                else if (ok == FC_GIVEUP) {
                    f  = THEORY;
                    m_incomplete_theories.push_back(th);
                }
            }
            else {
                ok = m_qmanager->final_check_eh(true);
                TRACE(final_check_step, tout << "quantifier  ok: " << ok << " " << "inconsistent " << inconsistent() << "\n";);
            }

            m_final_check_idx = (m_final_check_idx + 1) % range;
            // IF_VERBOSE(1000, verbose_stream() << "final check status: " << ok << "\n";);

            switch (ok) {
            case FC_DONE:
                break;
            case FC_GIVEUP:
                result = FC_GIVEUP;
                break;
            case FC_CONTINUE:
                return FC_CONTINUE;
                break;
            }
        }
        while (m_final_check_idx != old_idx);

        TRACE(final_check_step, tout << "result: " << result << "\n";);

        if (can_propagate()) {
            TRACE(final_check_step, tout << "can propagate: continue...\n";);
            return FC_CONTINUE;
        }

        SASSERT(result != FC_DONE || check_th_diseq_propagation());
        TRACE(final_check_step, tout << "RESULT final_check: " << result << "\n";);
        if (result == FC_GIVEUP && f != OK)
            m_last_search_failure = f;
        if (result == FC_DONE && has_lambda()) {
            m_last_search_failure = LAMBDAS;
            result = FC_GIVEUP;
        }
        return result;
    }

    void context::check_proof(proof * pr) {
        if (m.proofs_enabled() && m_fparams.m_check_proof) {
            proof_checker pf(m);
            expr_ref_vector side_conditions(m);
            pf.check(pr, side_conditions);
        }
    }

    void context::forget_phase_of_vars_in_current_level() {
        unsigned head = m_scope_lvl == 0 ? 0 : m_scopes[m_scope_lvl - 1].m_assigned_literals_lim;
        unsigned sz   = m_assigned_literals.size();
        for (unsigned i = head; i < sz; i++) {
            literal l  = m_assigned_literals[i];
            bool_var v = l.var();
            TRACE(forget_phase, tout << "forgetting phase of l: " << l << "\n";);
            m_bdata[v].m_phase_available = false;
        }
    }


    bool context::resolve_conflict() {
        m_stats.m_num_conflicts++;
        m_num_conflicts ++;
        m_num_conflicts_since_restart ++;
        m_num_conflicts_since_lemma_gc ++;
        switch (m_conflict.get_kind()) {
        case b_justification::CLAUSE:
        case b_justification::BIN_CLAUSE:
            m_stats.m_num_sat_conflicts++;
            break;
        default:
            break;
        }
        if (m_fparams.m_phase_selection == PS_THEORY || 
            m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE || 
            m_fparams.m_phase_selection == PS_CACHING_CONSERVATIVE2)
            forget_phase_of_vars_in_current_level();
        m_atom_propagation_queue.reset();
        m_eq_propagation_queue.reset();
        m_th_eq_propagation_queue.reset();
        m_th_diseq_propagation_queue.reset();
        if (m_conflict_resolution->resolve(m_conflict, m_not_l)) {
            unsigned new_lvl = m_conflict_resolution->get_new_scope_lvl();
            unsigned num_lits = m_conflict_resolution->get_lemma_num_literals();
            literal * lits    = m_conflict_resolution->get_lemma_literals();

            SASSERT(num_lits > 0);
            unsigned conflict_lvl = get_assign_level(lits[0]);
            SASSERT(conflict_lvl <= m_scope_lvl);

            // When num_lits == 1, then the default behavior is to go
            // to base-level. If the problem has quantifiers, it may be
            // too expensive to do that, since all instances will need to
            // be recreated. If that is the case, I store the assertions in
            // a special vector and keep reasserting whenever I backtrack.
            // Moreover, I backtrack only one level.
            bool delay_forced_restart =
                m_fparams.m_delay_units &&
                num_lits == 1 &&
                conflict_lvl > m_search_lvl + 1 &&
                !m.proofs_enabled() &&
                m_units_to_reassert.size() < m_fparams.m_delay_units_threshold;

            if (delay_forced_restart) {
                new_lvl = conflict_lvl - 1;
            }

            // Some of the literals/enodes of the conflict clause will be destroyed during
            // backtracking, and will need to be recreated. However, I want to keep
            // the generation number for enodes that are going to be recreated. See
            // comment in cache_generation(unsigned).
            if (m_conflict_resolution->get_lemma_intern_lvl() > new_lvl)
                cache_generation(num_lits, lits, new_lvl);

            SASSERT(new_lvl < m_scope_lvl);
            TRACE(resolve_conflict_bug,
                  tout << "m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << m_conflict_resolution->get_lemma_intern_lvl() << "\n";
                  tout << "num_lits: " << num_lits << "\n";
                  for (unsigned i = 0; i < num_lits; i++) {
                      literal l = lits[i];
                      tout << l << " ";
                      display_literal_smt2(tout, l);
                      tout << ", ilvl: " << get_intern_level(l.var()) << "\n"
                           << mk_pp(bool_var2expr(l.var()), m) << "\n";
                  });

            if (m.has_trace_stream() && !m_is_auxiliary) {
                m.trace_stream() << "[conflict] ";
                display_literals(m.trace_stream(), num_lits, lits);
                m.trace_stream() << "\n";
            }

#ifdef Z3DEBUG
            expr_ref_vector expr_lits(m);
            bool_vector   expr_signs;
            for (unsigned i = 0; i < num_lits; i++) {
                literal l = lits[i];
                if (get_assignment(l) != l_false) {
                    std::cout << l << " " << get_assignment(l) << "\n";
                }
                SASSERT(get_assignment(l) == l_false);
                expr_lits.push_back(bool_var2expr(l.var()));
                expr_signs.push_back(l.sign());
            }
#endif
            proof * pr = nullptr;
            if (m.proofs_enabled()) {
                pr = m_conflict_resolution->get_lemma_proof();
                // check_proof(pr);
                TRACE(context_proof, tout << mk_ll_pp(pr, m););
                TRACE(context_proof_hack,
                      static ast_mark visited;
                      ast_ll_pp(tout, m, pr, visited););
            }
            // I invoke pop_scope_core instead of pop_scope because I don't want
            // to reset cached generations... I need them to rebuild the literals
            // of the new conflict clause.
            if (relevancy()) record_relevancy(num_lits, lits);
            unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl);
            SASSERT(m_scope_lvl == new_lvl);
            // the logical context may still be in conflict after
            // clauses are reinitialized in pop_scope.
            if (m_conflict_resolution->get_lemma_intern_lvl() > m_scope_lvl) {
                expr * * atoms         = m_conflict_resolution->get_lemma_atoms();
                for (unsigned i = 0; i < num_lits; i++) {
                    literal l   = lits[i];
                    if (l.var() >= num_bool_vars) {
                        // This boolean variable was deleted during backtracking, it need to be recreated.
                        // Remark: atom may be a negative literal (not a). Z3 creates Boolean variables for not-gates that
                        // are nested in terms. Example: let f be a uninterpreted function from Bool -> Int.
                        // Then, given the term (f (not a)), Z3 will create a boolean variable for (not a) when internalizing (f (not a)).
                        expr * atom     = atoms[i];
                        internalize(atom, true);
                        // If atom is actually a negative literal (not a), then get_bool_var will return return null_bool_var.
                        // Thus, we must use get_literal instead. This was a bug/crash in Z3 <= 4.0
                        literal new_l = get_literal(atom);
                        if (l.sign())
                            new_l.neg();
                        // For reference, here is the buggy version
                        // BEGIN BUGGY VERSION
                        // bool_var v = get_bool_var(atom);
                        // CTRACE(resolve_conflict_crash, v == null_bool_var, tout << mk_ismt2_pp(atom, m) << "\n";);
                        // SASSERT(v != null_bool_var);
                        // literal new_l   = literal(v, l.sign());
                        // END BUGGY VERSION
                        lits[i]         = new_l;
                    }
                }
            }
            if (relevancy()) restore_relevancy(num_lits, lits);
            // Resetting the cache manually because I did not invoke pop_scope, but pop_scope_core
            reset_cache_generation();
            TRACE(resolve_conflict_bug,
                  tout << "AFTER m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " <<
                  m_conflict_resolution->get_lemma_intern_lvl() << "\n";
                  tout << "num_lits: " << num_lits << "\n";
                  for (unsigned i = 0; i < num_lits; i++) {
                      literal l = lits[i];
                      tout << l << " ";
                      display_literal(tout, l);
                      tout << ", ilvl: " << get_intern_level(l.var()) << "\n"
                           << mk_pp(bool_var2expr(l.var()), m) << "\n";
                  });
#ifdef Z3DEBUG
            for (unsigned i = 0; i < num_lits; i++) {
                literal l = lits[i];
                if (expr_signs[i] != l.sign()) {
                    expr* real_atom;
                    VERIFY(m.is_not(expr_lits.get(i), real_atom));
                    // the sign must have flipped when internalizing
                    CTRACE(resolve_conflict_bug, real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m) << "\n" << mk_pp(bool_var2expr(l.var()), m) << "\n";);
                    SASSERT(real_atom == bool_var2expr(l.var()));
                }
                else {
                    SASSERT(expr_lits.get(i) == bool_var2expr(l.var()));
                }
            }
#endif
            justification * js = nullptr;
            if (m.proofs_enabled()) {
                js = alloc(justification_proof_wrapper, *this, pr, false);
            }
#if 0
            {
                static unsigned counter = 0;
                static uint64_t total = 0;
                static unsigned max = 0;
                counter++;
                total += num_lits;
                if (num_lits > max) {
                    max = num_lits;
                }
                if (counter % 1000 == 0) {
                    verbose_stream() << "[sat] avg. clause size: " << ((double) total/(double) counter) << ", max: " << max << std::endl;
                    for (unsigned i = 0; i < num_lits; i++) {
                        literal l = lits[i];
                        verbose_stream() << l.sign() << " " << mk_pp(bool_var2expr(l.var()), m) << "\n";
                    }
                }
            }
#endif
            mk_clause(num_lits, lits, js, CLS_LEARNED);
            if (delay_forced_restart) {
                SASSERT(num_lits == 1);
                expr * unit     = bool_var2expr(lits[0].var());
                bool unit_sign  = lits[0].sign();
                while (m.is_not(unit, unit))
                    unit_sign = !unit_sign;
                m_units_to_reassert.push_back({ expr_ref(unit, m), unit_sign, is_relevant(unit) });
                TRACE(reassert_units, tout << "asserting " << mk_pp(unit, m) << " #" << unit->get_id() << " " << unit_sign << " @ " << m_scope_lvl << "\n";);
            }

            m_conflict_resolution->release_lemma_atoms();
            TRACE(context_lemma, tout << "new lemma: ";
                  literal_vector v(num_lits, lits);
                  std::sort(v.begin(), v.end());
                  for (unsigned i = 0; i < num_lits; i++) {
                      display_literal(tout, v[i]);
                      tout << "\n";
                      smt::display(tout, v[i], m, m_bool_var2expr.data());
                      tout << "\n\n";
                  }
                  tout << "\n";);
            decay_bvar_activity();
            update_phase_cache_counter();
            return true;
        }
        else if (m_fparams.m_clause_proof && !m.proofs_enabled()) {
            m_unsat_proof = m_clause_proof.get_proof(inconsistent());
        }
        else if (m.proofs_enabled()) {
            m_unsat_proof = m_conflict_resolution->get_lemma_proof();
            check_proof(m_unsat_proof);
        }
        return false;
    }

    /*
      \brief we record and restore relevancy information for literals in conflict clauses.
      A literal may have been marked relevant within the scope that gets popped during
      conflict resolution. In this case, the literal is no longer marked as relevant after
      the pop. This can cause quantifier instantiation to miss relevant triggers and thereby
      cause incompleteness.
     */
    void context::record_relevancy(unsigned n, literal const* lits) {
        m_relevant_conflict_literals.reset();
        for (unsigned i = 0; i < n; ++i) {
            m_relevant_conflict_literals.push_back(is_relevant(lits[i]));
        }
    }

    void context::restore_relevancy(unsigned n, literal const* lits) {
        for (unsigned i = 0; i < n; ++i) {
            if (m_relevant_conflict_literals[i] && !is_relevant(lits[i])) {
                mark_as_relevant(lits[i]);
            }
        }
    }

    void context::get_relevant_labels(expr* cnstr, buffer<symbol> & result) {
        if (m_fparams.m_check_at_labels) {
            check_at_labels checker(m);
            if (cnstr && !checker.check(cnstr)) {
                warning_msg("Boogie generated formula that can require multiple '@' labels in a counter-example");
            }
            else {
                unsigned nf = m_asserted_formulas.get_num_formulas();
                for (unsigned i = 0; i < nf; ++i) {
                    expr* fml = m_asserted_formulas.get_formula(i);
                    if (!checker.check(fml)) {
                        warning_msg("Boogie generated formula that can require multiple '@' labels in a counter-example");
                        break;
                    }
                }
            }
        }

        SASSERT(!inconsistent());
        for (expr * curr : m_b_internalized_stack) { 
            if (is_relevant(curr) && get_assignment(curr) == l_true) {
                // if curr is a label literal, then its tags will be copied to result.
                m.is_label_lit(curr, result);
            }
        }
    }

    /**
       \brief Collect relevant literals that may be used to block the current assignment.
       If at_lbls is true, then only labels that contains '@' are considered. (This is a hack for Boogie).
       This hack is also available in the Simplify theorem prover.
    */
    void context::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
        SASSERT(!inconsistent());
        buffer<symbol> lbls;
        for (expr * curr : m_b_internalized_stack) {
            if (is_relevant(curr) && get_assignment(curr) == l_true) {
                lbls.reset();
                if (m.is_label_lit(curr, lbls)) {
                    bool include = false;
                    if (at_lbls) {
                        // include if there is a label with the '@' sign.
                        for (symbol const& s : lbls) {
                            if (s.contains('@')) {
                                include = true;
                                break;
                            }
                        }
                    }
                    else {
                        include = true;
                    }
                    if (include)
                        result.push_back(curr);
                }
            }
        }
    }

    /**
       \brief Store in result the (relevant) literal assigned by the
       logical context.
    */
    void context::get_relevant_literals(expr_ref_vector & result) {
        SASSERT(!inconsistent());
        unsigned sz = m_b_internalized_stack.size();
        for (unsigned i = 0; i < sz; i++) {
            expr * curr = m_b_internalized_stack.get(i);
            if (is_relevant(curr)) {
                switch (get_assignment(curr)) {
                case l_true:
                    result.push_back(curr);
                    break;
                case l_false:
                    result.push_back(m.mk_not(curr));
                    break;
                default:
                    break;
                }
            }
        }
    }

    /**
       \brief Store the current set of guessed literals (i.e., case splits).
    */
    void context::get_guessed_literals(expr_ref_vector & result) {
        // The literals between [m_base_lvl, m_search_lvl) are not guesses but assumptions.
        SASSERT(m_base_lvl <= m_scopes.size());
        if (m_search_lvl == m_scopes.size()) {
            // do nothing... there are guesses...
        }
        for (unsigned i = m_search_lvl; i < m_scope_lvl; i++) {
            // This method assumes the first literal assigned in a non base scope level is a guess.
            scope & s          = m_scopes[i];
            unsigned guess_idx = s.m_assigned_literals_lim;
            literal guess      = m_assigned_literals[guess_idx];
            SASSERT(get_justification(guess.var()).get_kind() == b_justification::AXIOM);
            expr_ref lit(m);
            literal2expr(guess, lit);
            result.push_back(std::move(lit));
        }
    }

    /**
       \brief Undo object for bool var m_true_first field update.
    */
    class set_true_first_trail : public trail {
        context& ctx;
        bool_var m_var;
    public:
        set_true_first_trail(context& ctx, bool_var v): ctx(ctx), m_var(v) {}
        void undo() override {
            ctx.m_bdata[m_var].reset_true_first_flag();
        }
    };

    void context::set_true_first_flag(bool_var v) {
        push_trail(set_true_first_trail(*this, v));
        bool_var_data & d = m_bdata[v];
        d.set_true_first_flag();
    }

    bool context::assume_eq(enode * lhs, enode * rhs) {
        if (lhs->get_root() == rhs->get_root())
            return false; // it is not necessary to assume the eq.
        expr * _lhs = lhs->get_expr();
        expr * _rhs = rhs->get_expr();
        expr * eq = mk_eq_atom(_lhs, _rhs);
        TRACE(assume_eq, tout << "creating interface eq:\n" << mk_pp(eq, m) << "\n";);
        if (m.is_false(eq)) {
            return false;
        }
        bool r = false;
        if (!b_internalized(eq)) {
            // I do not invoke internalize(eq, true), because I want to
            // mark the try_true_first flag before invoking theory::internalize_eq_eh.
            // Reason: Theories like arithmetic should be able to know if the try_true_first flag is
            // marked or not. They use this information to also mark auxiliary atoms such as:
            //  (<= (- x y) 0)
            //  (>= (- y x) 0)
            // for the new equality atom (= x y).
            if (m.is_eq(eq)) {
                internalize_formula_core(to_app(eq), true);
                bool_var v        = get_bool_var(eq);
                bool_var_data & d = get_bdata(v);
                d.set_eq_flag();
                set_true_first_flag(v);
                sort * s    = to_app(eq)->get_arg(0)->get_sort();
                theory * th = m_theories.get_plugin(s->get_family_id());
                if (th)
                    th->internalize_eq_eh(to_app(eq), v);
            }
            else {
                internalize(eq, true);
            }
            r = true;
            m_stats.m_num_interface_eqs++;
            TRACE(assume_eq, tout << "new internalization.\n";);
        }
        bool_var v        = get_bool_var(eq);
        bool_var_data & d = m_bdata[v];
        if (!d.try_true_first()) {
            set_true_first_flag(v);
            r = true;
            TRACE(assume_eq, tout << "marked as ieq.\n";);
        }
        if (get_assignment(v) == l_undef) {
            TRACE(assume_eq, tout << "variable is unassigned.\n";);
            r = true;
        }
        if (relevancy() && !is_relevant(eq)) {
            TRACE(assume_eq, tout << "marking eq as relevant.\n";);
            mark_as_relevant(eq);
            r = true;
        }
        TRACE(assume_eq, tout << "variable value: " << get_assignment(v) << "\n";);
        TRACE(assume_eq, tout << "assume_eq result: " << r << "\n";);
        return r;
    }

    bool context::is_shared(enode * n) const {
        n = n->get_root();
        switch (n->is_shared()) {
        case l_true: return true;
        case l_false: return false;
        default: break;
        }

        unsigned num_th_vars = n->get_num_th_vars();
        if (m.is_ite(n->get_expr())) {
            n->set_is_shared(l_true);
            return true;
        }
        switch (num_th_vars) {
        case 0: {
            return false;
        }
        case 1: {
            if (m_qmanager->is_shared(n) && !m.is_lambda_def(n->get_expr()) && !m_lambdas.contains(n)) 
                return true;

            // the variable is shared if the equivalence class of n
            // contains a parent application.

            theory_var_list * l = n->get_th_var_list();
            theory_id th_id     = l->get_id();

            for (enode * parent : enode::parents(n)) {
                app* p = parent->get_expr();
                family_id fid = p->get_family_id();
                if (fid != th_id && fid != m.get_basic_family_id()) {
                    if (is_beta_redex(parent, n))
                        continue;
                    TRACE(is_shared, tout << enode_pp(n, *this) 
                          << "\nis shared because of:\n" 
                          << enode_pp(parent, *this) << "\n";);
                    n->set_is_shared(l_true);
                    return true;
                }
            }

            // Some theories implement families of theories. Examples:
            // Arrays and Tuples.  For example, array theory is a
            // parametric theory, that is, it implements several theories:
            // (array int int), (array int (array int int)), ...
            //
            // Example:
            //
            // a : (array int int)
            // b : (array int int)
            // x : int
            // y : int
            // v : int
            // w : int
            // A : (array (array int int) int)
            //
            // assert (= b (store a x v))
            // assert (= b (store a y w))
            // assert (not (= x y))
            // assert (not (select A a))
            // assert (not (select A b))
            // check
            //
            // In the example above, 'a' and 'b' are shared variables between
            // the theories of (array int int) and (array (array int int) int).
            // Remark: The inconsistency is not going to be detected if they are
            // not marked as shared.
            bool r = get_theory(th_id)->is_shared(l->get_var());
            n->set_is_shared(to_lbool(r));
            return r;
        }
        default:
            return true;
        }
    }

    bool context::is_beta_redex(enode* p, enode* n) const {
        family_id th_id = p->get_expr()->get_family_id();
        theory * th = get_theory(th_id);
        return th && th->is_beta_redex(p, n);
    }

    bool context::get_value(enode * n, expr_ref & value) {
        sort * s      = n->get_sort();
        family_id fid = s->get_family_id();
        theory * th   = get_theory(fid);
        if (th == nullptr)
            return false;
        return th->get_value(n, value);
    }   

    void context::solve_for(vector<solution>& sol) {
        for (auto th : m_theories)
            if (th)
                th->solve_for(sol);
    }

    bool context::update_model(bool refinalize) {
        final_check_status fcs = FC_DONE;
        if (refinalize) {
            if (has_case_splits())
                return false;
            fcs = final_check();
            TRACE(opt, tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";);
        }
        if (fcs == FC_DONE) {
            reset_model();
        }
        return false;
    }

    void context::mk_proto_model() {
        if (m_model || m_proto_model || has_case_splits()) return;
        TRACE(get_model,
              display(tout);
              display_normalized_enodes(tout);
              display_enodes_lbls(tout);
              m_fingerprints.display(tout);
              );
        failure fl = get_last_search_failure();
        if (fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) {
            TRACE(get_model, tout << "last search failure: " << fl << "\n";);   
        }     
        else if (m_fparams.m_model || m_fparams.m_model_on_final_check || 
                 (m_qmanager->has_quantifiers() && m_qmanager->model_based())) {
            m_model_generator->reset();
            m_proto_model = m_model_generator->mk_model();
            m_qmanager->adjust_model(m_proto_model.get());
            TRACE(mbqi_bug, tout << "before complete_partial_funcs:\n"; model_pp(tout, *m_proto_model););
            m_proto_model->complete_partial_funcs(false);
            TRACE(mbqi_bug, tout << "before cleanup:\n"; model_pp(tout, *m_proto_model););
            m_proto_model->cleanup();
            TRACE(mbqi_bug, tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
            IF_VERBOSE(11, model_pp(verbose_stream(), *m_proto_model););
        }
    }

    proof * context::get_proof() {        
        if (!m_unsat_proof) {
            m_unsat_proof = m_clause_proof.get_proof(inconsistent());
        }
        TRACE(context, tout << m_unsat_proof << "\n";);
        return m_unsat_proof;
    }

    bool context::has_case_splits() {
        if (!m_has_case_split)
            return false;
        
        for (unsigned i = get_num_b_internalized(); i-- > 0; ) {
            if (is_relevant(i) && get_assignment(i) == l_undef)
                return true;
        }
        return false;
    }

    void context::get_model(model_ref & mdl) {
        if (inconsistent())
            mdl = nullptr;
        else if (m_model.get())
            mdl = m_model.get();
        else if (!m.inc())
            mdl = nullptr;
        else if (!m_search_finalized)
            mdl = nullptr;
        else {
            mk_proto_model();
            if (!m_model && m_proto_model) {
                m_model = m_proto_model->mk_model();
                try {
                    add_rec_funs_to_model();
                }
                catch (...) {
                    // no op
                }                
            }
            mdl = m_model.get();
        }
        if (m_fmls && mdl) {
            auto convert = m_fmls->model_trail().get_model_converter();
            if (convert)
                (*convert)(mdl);
        }
    }

    void context::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
        unsigned sz = vars.size(); 
        depth.resize(sz);
        for (unsigned i = 0; i < sz; ++i) {
            expr* v = vars[i];
            bool_var bv = m_expr2bool_var.get(v->get_id(), null_bool_var);
            depth[i] = bv == null_bool_var ? UINT_MAX : get_assign_level(bv);            
        }
    }

    expr_ref_vector context::get_trail(unsigned max_level) {        
        expr_ref_vector result(get_manager());
        for (literal lit : m_assigned_literals) {
            if (get_assign_level(lit) > max_level + m_base_lvl)
                continue;
            expr_ref e(m);
            literal2expr(lit, e);
            result.push_back(std::move(e));
        }
        return result;
    }

    void context::get_units(expr_ref_vector& result) {
        expr_mark visited;
        for (expr* fml : result)
            visited.mark(fml);
        expr_ref_vector trail = get_trail(0);
        for (expr* t : trail) 
            if (!visited.is_marked(t))
                result.push_back(t);
    }


    failure context::get_last_search_failure() const {
        return m_last_search_failure;
    }

    void context::add_rec_funs_to_model() {
        model_params p;
        auto smtlib2_compliant = gparams::get_value("smtlib2_compliant");
        
        if (m_model && p.user_functions() && smtlib2_compliant != "true")
            m_model->add_rec_funs();
    }

};


#ifdef Z3DEBUG
void pp(smt::context & c) {
    c.display(std::cout);
}
#endif