diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 82ab483aa..a93b6258d 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -822,3 +822,8 @@ func_decl* arith_util::mk_div0() {
     sort* rs[2] = { mk_real(), mk_real() };
     return m_manager.mk_func_decl(m_afid, OP_DIV0, 0, nullptr, 2, rs, mk_real());
 }
+
+func_decl* arith_util::mk_idiv0() {
+    sort* rs[2] = { mk_int(), mk_int() };
+    return m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
+}
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 0bc572feb..86241a1fa 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -368,6 +368,7 @@ public:
     sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); }
 
     func_decl* mk_div0();
+    func_decl* mk_idiv0();
 
 
     app * mk_numeral(rational const & val, bool is_int) const {
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 1f467999e..f6e038d60 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -193,7 +193,7 @@ struct purify_arith_proc {
         expr_ref_vector      m_pinned;
         expr_ref_vector      m_new_cnstrs;
         proof_ref_vector     m_new_cnstr_prs;
-        svector<div_def>     m_divs;
+        svector<div_def>     m_divs, m_idivs;
         expr_ref             m_subst;
         proof_ref            m_subst_pr;
         expr_ref_vector      m_new_vars;
@@ -361,6 +361,7 @@ struct purify_arith_proc {
                 push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero))));
                 push_cnstr_pr(mod_pr);
             }
+            m_idivs.push_back(div_def(x, y, k1));
         }
    
         void process_mod(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { 
@@ -775,6 +776,7 @@ struct purify_arith_proc {
             m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : nullptr, nullptr);
         }
         auto const& divs = r.cfg().m_divs;
+        auto const& idivs = r.cfg().m_idivs;
         for (unsigned i = 0; i < divs.size(); ++i) {
             auto const& p1 = divs[i];
             for (unsigned j = i + 1; j < divs.size(); ++j) {
@@ -784,6 +786,15 @@ struct purify_arith_proc {
                                        m().mk_eq(p1.d, p2.d)));
             }
         }
+        for (unsigned i = 0; i < idivs.size(); ++i) {
+            auto const& p1 = idivs[i];
+            for (unsigned j = i + 1; j < idivs.size(); ++j) {
+                auto const& p2 = idivs[j];
+                m_goal.assert_expr(m().mk_implies(
+                                       m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), 
+                                       m().mk_eq(p1.d, p2.d)));
+            }
+        }
         
         // add generic_model_converter to eliminate auxiliary variables from model
         if (produce_models) {
@@ -804,6 +815,15 @@ struct purify_arith_proc {
                 }
                 fmc->add(u().mk_div0(), body);
             }
+            if (!idivs.empty()) {
+                expr_ref body(u().mk_int(0), m());
+                expr_ref v0(m().mk_var(0, u().mk_int()), m());
+                expr_ref v1(m().mk_var(1, u().mk_int()), m());
+                for (auto const& p : idivs) {
+                    body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body);
+                }
+                fmc->add(u().mk_idiv0(), body);
+            }
         }
         if (produce_models && !m_sin_cos.empty()) {
             generic_model_converter* emc = alloc(generic_model_converter, m(), "purify_sin_cos");
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 90fcc14cf..f98c848a0 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -789,10 +789,8 @@ namespace smtfd {
                 expr_ref v = eval_abs(t);
                 val2elem_t& v2e = get_table(s);
                 expr* e;
-                if (v2e.find(v, e)) {
-                    if (e != t) {
-                        m_context.add(m.mk_not(m.mk_eq(e, t)), __FUNCTION__);
-                    }
+                if (v2e.find(v, e) && e != t && m.is_value(e)) {
+                    m_context.add(m.mk_not(m.mk_eq(e, t)), __FUNCTION__);
                 }
                 else {
                     m_pinned.push_back(v);
@@ -1333,22 +1331,23 @@ namespace smtfd {
                 }
             }
         }
-
     };
 
+
     class mbqi {
-        ast_manager&    m;
-        plugin_context& m_context;
-        obj_hashtable<quantifier>& m_enforced;
-        model_ref       m_model;
-        ref<::solver>   m_solver;
-        expr_ref_vector m_pinned;
+        ast_manager&                    m;
+        plugin_context&                 m_context;
+        obj_hashtable<quantifier>       m_enforced;
+        model_ref                       m_model;
+        ref<::solver>                   m_solver;
         obj_pair_map<expr, sort, expr*> m_val2term;
+        expr_ref_vector                 m_val2term_trail;
+        obj_map<sort, expr*>            m_fresh;
+        expr_ref_vector                 m_fresh_trail;
 
         expr* abs(expr* e) { return m_context.get_abs().abs(e);  }
         expr_ref eval_abs(expr* t) { return (*m_model)(abs(t)); }
 
-
         void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe) {
             SASSERT(!universe.empty());
             expr_ref_vector eqs(m);
@@ -1359,6 +1358,32 @@ namespace smtfd {
             m_solver->assert_expr(fml);
         }
 
+        expr_ref fresh(sort* s) {
+            expr* e = nullptr;
+            if (!m_fresh.find(s, e)) {
+                e = m.mk_fresh_const(s->get_name(), s, false);
+                m_fresh.insert(s, e);
+                m_fresh_trail.push_back(e);
+            }
+            return expr_ref(e, m);
+        }
+
+        expr_ref replace_model_value(expr* e) {
+            if (m.is_model_value(e)) {                
+                expr_ref r = fresh(m.get_sort(e));
+                std::cout << expr_ref(e, m) << " |-> " << r << "\n";
+                return r;
+            }
+            if (is_app(e) && to_app(e)->get_num_args() > 0) {
+                expr_ref_vector args(m);
+                for (expr* arg : *to_app(e)) {
+                    args.push_back(replace_model_value(arg));
+                }
+                return expr_ref(m.mk_app(to_app(e)->get_decl(), args.size(), args.c_ptr()), m);
+            }
+            return expr_ref(e, m);
+        }
+
         // !Ex P(x) => !P(t)
         // Ax P(x) => P(t)
         // l_true: new instance
@@ -1408,11 +1433,7 @@ namespace smtfd {
             if (r == l_true) {
                 expr_ref qq(q->get_expr(), m);
                 for (expr* t : subterms(qq)) {
-                    if (is_ground(t)) {                       
-                        expr_ref v = eval_abs(t);
-                        m_pinned.push_back(v);
-                        m_val2term.insert(v, m.get_sort(t), t);
-                    }
+                    init_term(t);
                 }
                 m_solver->get_model(mdl);
                 TRACE("smtfd", tout << *mdl << "\n";);
@@ -1429,6 +1450,9 @@ namespace smtfd {
                     if (m_val2term.find(val, m.get_sort(v), t)) {
                         val = t;
                     }
+                    else {
+                        val = replace_model_value(val);
+                    }
                     vals[i] = val;
                 }
             }
@@ -1443,12 +1467,14 @@ namespace smtfd {
                 else {
                     body = m.mk_implies(body, q);
                 }
+                IF_VERBOSE(1, verbose_stream() << body << "\n");
                 m_context.add(body, __FUNCTION__);
             }
             m_solver->pop(1);
             return r;
         }
 
+        // 
         lbool check_exists(quantifier* q) {
             if (m_enforced.contains(q)) {
                 return l_true;
@@ -1473,36 +1499,51 @@ namespace smtfd {
             return l_true;
         }
 
-        void init_val2term(expr_ref_vector const& core) {
-            for (expr* t : subterms(core)) {
-                if (!m.is_bool(t) && is_ground(t)) {
-                    expr_ref v = eval_abs(t);
-                    m_pinned.push_back(v);
+        void init_term(expr* t) {
+            if (!m.is_bool(t) && is_ground(t)) {
+                expr_ref v = eval_abs(t);
+                if (!m_val2term.contains(v, m.get_sort(t))) {
                     m_val2term.insert(v, m.get_sort(t), t);
+                    m_val2term_trail.push_back(v);
                 }
             }
         }
 
     public:
 
-        mbqi(::solver* s, plugin_context& c, obj_hashtable<quantifier>& enforced, model_ref& mdl):
-            m(s->get_manager()),
+        mbqi(plugin_context& c):
+            m(c.get_manager()),
             m_context(c),
-            m_enforced(enforced),
-            m_model(mdl),
-            m_solver(s),
-            m_pinned(m)
+            m_model(nullptr),
+            m_solver(nullptr),
+            m_val2term_trail(m),
+            m_fresh_trail(m)
         {}
+
+        void set_model(model* mdl) { m_model = mdl; }
+
+        ref<::solver> & get_solver() { return m_solver; }
             
+        void init_val2term(expr_ref_vector const& fmls, expr_ref_vector const& core) {
+            m_val2term_trail.reset();
+            m_val2term.reset();
+            for (expr* t : subterms(core)) {
+                init_term(t);
+            }
+            for (expr* t : subterms(fmls)) {
+                init_term(t);
+            }
+        }
+
         bool check_quantifiers(expr_ref_vector const& core) {
             bool result = true;
-            init_val2term(core);
             IF_VERBOSE(9, 
                        for (expr* c : core) {
                            verbose_stream() << "core: " << mk_bounded_pp(c, m, 2) << "\n";
                        });
             for (expr* c : core) {
                 lbool r = l_false;
+                IF_VERBOSE(1, verbose_stream() << "core: " << mk_bounded_pp(c, m, 2) << "\n");
                 if (is_forall(c)) {
                     r = check_forall(to_quantifier(c));
                 }
@@ -1536,6 +1577,7 @@ namespace smtfd {
     class solver : public solver_na2as {
         ast_manager&    m;
         mutable smtfd_abs       m_abs;
+        unsigned        m_indent;
         plugin_context  m_context;
         uf_plugin       m_uf;
         ar_plugin       m_ar;
@@ -1545,18 +1587,18 @@ namespace smtfd {
         ref<::solver>   m_fd_sat_solver;
         ref<::solver>   m_fd_core_solver;
         ref<::solver>   m_smt_solver;
-        ref<solver>     m_mbqi_solver;
+        mbqi            m_mbqi;
         expr_ref_vector m_assertions;
         unsigned_vector m_assertions_lim;
         unsigned        m_assertions_qhead;
         expr_ref_vector m_axioms;
+        unsigned_vector m_axioms_lim;
         expr_ref_vector m_toggles;
         unsigned_vector m_toggles_lim;
         model_ref       m_model;
         std::string     m_reason_unknown;
         stats           m_stats;
         unsigned        m_max_conflicts;
-        obj_hashtable<quantifier> m_enforced_quantifier;
 
         void set_delay_simplify() {
             params_ref p;
@@ -1574,6 +1616,10 @@ namespace smtfd {
             return m_toggles.contains(e);
         }
 
+        void indent() {
+            for (unsigned i = 0; i < m_indent; ++i) verbose_stream() << " ";
+        }
+
         void flush_assertions() {
             SASSERT(m_assertions_qhead <= m_assertions.size());
             unsigned sz = m_assertions.size() - m_assertions_qhead;
@@ -1629,7 +1675,7 @@ namespace smtfd {
         }
 
         lbool check_smt(expr_ref_vector& core) {
-            IF_VERBOSE(10, verbose_stream() << "core: " << core.size() << "\n");
+            IF_VERBOSE(10, indent(); verbose_stream() << "core: " << core.size() << "\n");
             params_ref p;
             p.set_uint("max_conflicts", m_max_conflicts);
             m_smt_solver->updt_params(p);
@@ -1709,15 +1755,18 @@ namespace smtfd {
                           tout << m_context.term_covered(a) << " " << m_context.sort_covered(m.get_sort(a)) << "\n";
                       }
                   }
-                  tout << "has quantifier: " << has_q << "\n" << core << "\n";);
+                  tout << "has quantifier: " << has_q << "\n" << core << "\n";
+                  tout << *m_model.get() << "\n";
+                  );
             if (!has_q) {
                 return is_decided;
             }
-            if (!m_mbqi_solver) {
-                m_mbqi_solver = alloc(solver, m, get_params());
+            m_mbqi.set_model(m_model.get());
+            if (!m_mbqi.get_solver()) {
+                m_mbqi.get_solver() = alloc(solver, m_indent + 1, m, get_params());
             }
-            mbqi mb(m_mbqi_solver.get(), m_context, m_enforced_quantifier, m_model);
-            if (!mb.check_quantifiers(core) && m_context.empty()) {
+            m_mbqi.init_val2term(m_assertions, core);
+            if (!m_mbqi.check_quantifiers(core) && m_context.empty()) {
                 return l_false;
             }
             for (expr* f : m_context) {
@@ -1791,9 +1840,10 @@ namespace smtfd {
         }
         
     public:
-        solver(ast_manager& m, params_ref const& p):
+        solver(unsigned indent, ast_manager& m, params_ref const& p):
             solver_na2as(m),
             m(m),
+            m_indent(indent),
             m_abs(m),
             m_context(m_abs, m),
             m_uf(m_context),
@@ -1801,6 +1851,7 @@ namespace smtfd {
             m_bv(m_context),
             m_bs(m_context),
             m_pb(m_context),
+            m_mbqi(m_context),
             m_assertions(m),
             m_assertions_qhead(0),
             m_axioms(m),
@@ -1814,7 +1865,7 @@ namespace smtfd {
         ~solver() override {}
         
         ::solver* translate(ast_manager& dst_m, params_ref const& p) override {
-            solver* result = alloc(solver, dst_m, p);
+            solver* result = alloc(solver, m_indent, dst_m, p);
             if (m_smt_solver) result->m_smt_solver = m_smt_solver->translate(dst_m, p);
             if (m_fd_sat_solver) result->m_fd_sat_solver = m_fd_sat_solver->translate(dst_m, p);
             if (m_fd_core_solver) result->m_fd_core_solver = m_fd_core_solver->translate(dst_m, p);
@@ -1833,6 +1884,7 @@ namespace smtfd {
             m_fd_core_solver->push();
             m_smt_solver->push();
             m_assertions_lim.push_back(m_assertions.size());
+            m_axioms_lim.push_back(m_axioms.size());
             m_toggles_lim.push_back(m_toggles.size());
         }
         
@@ -1846,6 +1898,8 @@ namespace smtfd {
             m_toggles_lim.shrink(m_toggles_lim.size() - n);
             m_assertions.shrink(m_assertions_lim[m_assertions_lim.size() - n]);
             m_assertions_lim.shrink(m_assertions_lim.size() - n);
+            m_axioms.shrink(m_axioms_lim[m_axioms_lim.size() - n]);
+            m_axioms_lim.shrink(m_axioms_lim.size() - n);
             m_assertions_qhead = m_assertions.size();
         }
 
@@ -1861,6 +1915,11 @@ namespace smtfd {
         void assert_fd(expr* fml) {
             expr_ref _fml(fml, m);
             TRACE("smtfd", tout << mk_bounded_pp(fml, m, 3) << "\n";);
+            CTRACE("smtfd", m_axioms.contains(fml), 
+                   tout << "formula:\n" << _fml << "\n";
+                   tout << "axioms:\n" << m_axioms << "\n";
+                   tout << "assertions:\n" << m_assertions << "\n";);
+
             SASSERT(!m_axioms.contains(fml));
             m_axioms.push_back(fml);
             _fml = abs(fml);
@@ -1882,7 +1941,7 @@ namespace smtfd {
             lbool r = l_undef;
             expr_ref_vector core(m), axioms(m);
             while (true) {
-                IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat :rounds " << m_stats.m_num_rounds 
+                IF_VERBOSE(1, indent(); verbose_stream() << "(smtfd-check-sat :rounds " << m_stats.m_num_rounds 
                            << " :lemmas " << m_stats.m_num_lemmas << " :qi " << m_stats.m_num_mbqi << ")\n");
                 m_stats.m_num_rounds++;
                 checkpoint();
@@ -1949,7 +2008,7 @@ namespace smtfd {
                     ++round;
                     continue;
                 }
-                IF_VERBOSE(1, verbose_stream() << "(smtfd-round :round " << round << " :lemmas " << m_context.size() << ")\n");
+                IF_VERBOSE(1, indent(); verbose_stream() << "(smtfd-round :round " << round << " :lemmas " << m_context.size() << ")\n");
                 round = 0;
                 TRACE("smtfd_verbose", 
                       for (expr* f : m_context) tout << "refine " << mk_bounded_pp(f, m, 3) << "\n";
@@ -2059,7 +2118,7 @@ namespace smtfd {
 }
 
 solver * mk_smtfd_solver(ast_manager & m, params_ref const & p) {
-    return alloc(smtfd::solver, m, p);
+    return alloc(smtfd::solver, 0, m, p);
 }
 
 tactic * mk_smtfd_tactic(ast_manager & m, params_ref const & p) {
diff --git a/src/util/parray.h b/src/util/parray.h
index 38d6987d0..d02d47c83 100644
--- a/src/util/parray.h
+++ b/src/util/parray.h
@@ -216,9 +216,7 @@ private:
         unsigned sz = r->m_size;
         vs = nullptr;
         copy_values(r->m_values, sz, vs);
-        unsigned i = cs.size();
-        while (i > 0) {
-            --i;
+        for (unsigned i = cs.size(); i-- > 0; ) {
             cell * curr = cs[i];
             switch (curr->kind()) {
             case SET:
@@ -312,6 +310,26 @@ public:
         }
     }
 
+    void check_size(cell* c) const {
+        unsigned r;
+        while (c) {
+            switch (c->kind()) {
+            case SET:
+                break;
+            case PUSH_BACK:
+                r = size(c->next());
+                break;
+            case POP_BACK:
+                r = size(c->next());
+                SASSERT(c->idx() == r);
+                break;
+            case ROOT:
+                return;
+            }
+            c = c->next();
+        }
+    }
+
     bool empty(ref const & r) const { return size(r) == 0; }
 
     value const & get(ref const & r, unsigned i) const {
@@ -528,7 +546,7 @@ public:
         unsigned r_sz = size(r);
         unsigned trail_split_idx = r_sz / C::factor;
         unsigned i = 0;
-        cell * c   = r.m_ref;
+        cell * c   = r.m_ref;        
         while (c->kind() != ROOT && i < trail_split_idx) {
             cs.push_back(c);
             c = c->next();
@@ -538,10 +556,9 @@ public:
             // root is too far away.
             unfold(c);
         }
-        SASSERT(c->kind() == ROOT);
-        i = cs.size();
-        while (i > 0) {
-            --i;
+        DEBUG_CODE(check_size(c););
+        SASSERT(c->kind() == ROOT);      
+        for (i = cs.size(); i-- > 0; ) {
             cell * p = cs[i];
             SASSERT(c->m_kind == ROOT);
             unsigned sz = c->m_size;
@@ -558,10 +575,10 @@ public:
             case PUSH_BACK:
                 c->m_kind = POP_BACK;
                 if (sz == capacity(vs))
-                    expand(vs);
-                c->m_idx  = sz;
-                vs[sz]    = p->m_elem;
-                sz++;
+                    expand(vs);                
+                vs[sz] = p->m_elem;
+                ++sz;
+                c->m_idx = sz;
                 break;
             case POP_BACK:
                 c->m_kind = PUSH_BACK;
@@ -575,11 +592,12 @@ public:
             }
             inc_ref(p);
             c->m_next   = p;
-            // p does not point to c anymore
-            dec_ref(c);
+
             p->m_kind   = ROOT;
             p->m_size   = sz;
             p->m_values = vs;
+            // p does not point to c anymore
+            dec_ref(c);
             c = p;
         }
         SASSERT(c == r.m_ref);
@@ -604,9 +622,11 @@ public:
             case ROOT: out << "root, " << c->m_size << ", " << capacity(c->m_values); break;
             }
             out << "]#" << c->m_ref_count;
-            if (c->kind() == ROOT)
+            if (c->kind() == ROOT) {
+                out << "\n";
                 break;
-            out << " -> ";
+            }
+            out << " -> \n";
             c = c->next();
         }
     }