diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index c84b69c3c..c512d58af 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -53,11 +53,11 @@ extern "C" {
         RESET_ERROR_CODE();
         if (i < 0 || (size_t)i >= (SIZE_MAX >> PTR_ALIGNMENT)) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
-            return nullptr;
+            return of_symbol(symbol::null);
         }
-        Z3_symbol result = of_symbol(symbol(i));
+        Z3_symbol result = of_symbol(symbol((unsigned)i));
         return result;
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
     }
 
     Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, char const * str) {
@@ -71,7 +71,7 @@ extern "C" {
             s = symbol(str);
         Z3_symbol result = of_symbol(s);
         return result;
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
     }
 
     bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2) {
@@ -437,7 +437,7 @@ extern "C" {
     Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d) {
         LOG_Z3_get_decl_name(c, d);
         RESET_ERROR_CODE();
-        CHECK_VALID_AST(d, nullptr);
+        CHECK_VALID_AST(d, of_symbol(symbol::null));
         return of_symbol(to_func_decl(d)->get_name());
     }
 
@@ -521,18 +521,18 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_decl_symbol_parameter(c, d, idx);
         RESET_ERROR_CODE();
-        CHECK_VALID_AST(d, nullptr);
+        CHECK_VALID_AST(d, of_symbol(symbol::null));
         if (idx >= to_func_decl(d)->get_num_parameters()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
-            return nullptr;
+            return of_symbol(symbol::null);
         }
         parameter const& p = to_func_decl(d)->get_parameters()[idx];
         if (!p.is_symbol()) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return nullptr;
+            return of_symbol(symbol::null);
         }
         return of_symbol(p.get_symbol());
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
     }
 
     Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx) {
@@ -612,9 +612,9 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_sort_name(c, t);
         RESET_ERROR_CODE();
-        CHECK_VALID_AST(t, nullptr);
+        CHECK_VALID_AST(t, of_symbol(symbol::null));
         return of_symbol(to_sort(t)->get_name());
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
     }
 
     Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a) {
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 09106c9ec..4b29a66d6 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -679,8 +679,8 @@ extern "C" {
         for (unsigned i = 0; i < names.size(); ++i) {
             ss << ";" << names[i].str();
         }
-        RETURN_Z3(of_symbol(symbol(ss.str().substr(1).c_str())));
-        Z3_CATCH_RETURN(nullptr);
+        return of_symbol(symbol(ss.str().substr(1).c_str()));
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
     }
 
     void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) {
diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp
index b2fa2e815..4d10eff8a 100644
--- a/src/api/api_params.cpp
+++ b/src/api/api_params.cpp
@@ -172,11 +172,11 @@ extern "C" {
         RESET_ERROR_CODE();
         if (i >= to_param_descrs_ptr(p)->size()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
-            RETURN_Z3(nullptr);
+            return of_symbol(symbol::null);
         }
         Z3_symbol result = of_symbol(to_param_descrs_ptr(p)->get_param_name(i));
         return result;
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
     }
 
     Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s) {
diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp
index ab9c165a1..25d31229f 100644
--- a/src/api/api_quant.cpp
+++ b/src/api/api_quant.cpp
@@ -37,8 +37,8 @@ extern "C" {
             c,
             is_forall,
             weight,
-            nullptr,
-            nullptr,
+            of_symbol(symbol::null),
+            of_symbol(symbol::null),
             num_patterns, patterns,
             0, nullptr,
             num_decls, sorts,
@@ -290,7 +290,7 @@ extern "C" {
                                          unsigned num_patterns,
                                          Z3_pattern const patterns[],
                                          Z3_ast body) {
-        return Z3_mk_quantifier_const_ex(c, is_forall, weight, nullptr, nullptr,
+        return Z3_mk_quantifier_const_ex(c, is_forall, weight, of_symbol(symbol::null), of_symbol(symbol::null),
                                          num_bound, bound,
                                          num_patterns, patterns,
                                          0, nullptr,
@@ -456,9 +456,9 @@ extern "C" {
         }
         else {
             SET_ERROR_CODE(Z3_SORT_ERROR, nullptr);
-            return nullptr;
+            return of_symbol(symbol::null);
         }
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(of_symbol(symbol::null));
     }
 
     Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i) {
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 9d1006e2a..6052727e3 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -427,7 +427,7 @@ namespace z3 {
         if (s.kind() == Z3_INT_SYMBOL)
             out << "k!" << s.to_int();
         else
-            out << s.str().c_str();
+            out << s.str();
         return out;
     }
 
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 9be1b79c2..5ec895a07 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -762,7 +762,7 @@ namespace datatype {
     }
 
     bool util::is_declared(sort* s) const {
-        return m_plugin->is_declared(s);
+        return plugin().is_declared(s);
     }
     
     void util::compute_datatype_size_functions(svector<symbol> const& names) {
@@ -918,7 +918,7 @@ namespace datatype {
     }
 
     def const& util::get_def(sort* s) const {
-        return m_plugin->get_def(s);
+        return plugin().get_def(s);
     }
 
     void util::get_subsorts(sort* s, ptr_vector<sort>& sorts) const {
@@ -933,13 +933,25 @@ namespace datatype {
 
     util::util(ast_manager & m):
         m(m),
-        m_family_id(m.mk_family_id("datatype")),
+        m_family_id(null_family_id),
+        m_plugin(nullptr),
         m_asts(m),
         m_start(0) {
-        m_plugin = dynamic_cast<decl::plugin*>(m.get_plugin(m_family_id));
-        SASSERT(m_plugin);
     }
 
+
+    decl::plugin& util::plugin() const {
+        if (!m_plugin) m_plugin = dynamic_cast<decl::plugin*>(m.get_plugin(fid()));
+        SASSERT(m_plugin);
+        return *m_plugin;
+    }
+
+    family_id util::fid() const {
+        if (m_family_id == null_family_id) m_family_id = m.get_family_id("datatype");
+        return m_family_id;
+    }
+
+
     util::~util() {
         std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
     }
@@ -994,7 +1006,7 @@ namespace datatype {
         SASSERT(is_constructor(con));
         sort * datatype = con->get_range();
         parameter ps[1] = { parameter(con)};
-        return m.mk_func_decl(m_family_id, OP_DT_IS, 1, ps, 1, &datatype);
+        return m.mk_func_decl(fid(), OP_DT_IS, 1, ps, 1, &datatype);
     }
 
     func_decl * util::get_constructor_recognizer(func_decl * con) {
@@ -1011,7 +1023,7 @@ namespace datatype {
             }
         }
         parameter ps[2] = { parameter(con), parameter(r) };
-        d  = m.mk_func_decl(m_family_id, OP_DT_RECOGNISER, 2, ps, 1, &datatype);
+        d  = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype);
         SASSERT(d);
         m_asts.push_back(con);
         m_asts.push_back(d);
@@ -1226,7 +1238,7 @@ namespace datatype {
         while (!todo.empty()) {
             sort* s = todo.back();
             todo.pop_back();
-            defs.push_back(&m_plugin->get_def(s->get_name()));
+            defs.push_back(&plugin().get_def(s->get_name()));
             def const& d = get_def(s);
             for (constructor* c : d) {
                 for (accessor* a : *c) {
@@ -1281,7 +1293,7 @@ namespace datatype {
             mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr),
             mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail)
         };
-        decl::plugin& p = *get_plugin();
+        decl::plugin& p = plugin();
 
         sort_ref_vector sorts(m);
         datatype_decl * decl = mk_datatype_decl(*this, name, 0, nullptr, 2, constrs);
@@ -1313,7 +1325,7 @@ namespace datatype {
         auto * p = mk_constructor_decl(symbol("pair"), symbol("is-pair"), 2, accd);
         auto* dt = mk_datatype_decl(*this, symbol("pair"), 0, nullptr, 1, &p);
         sort_ref_vector sorts(m);
-        VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts));
+        VERIFY(plugin().mk_datatypes(1, &dt, 0, nullptr, sorts));
         del_datatype_decl(dt);
         sort* s = sorts.get(0);
         ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
@@ -1335,7 +1347,7 @@ namespace datatype {
         auto* tuple = mk_constructor_decl(name, test, accd.size(), accd.c_ptr());
         auto* dt = mk_datatype_decl(*this, name, 0, nullptr, 1, &tuple);
         sort_ref_vector sorts(m);
-        VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts));
+        VERIFY(plugin().mk_datatypes(1, &dt, 0, nullptr, sorts));
         del_datatype_decl(dt);
         sort* s = sorts.get(0);
         ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
@@ -1349,8 +1361,8 @@ namespace datatype {
 }
 
 datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) {
-    datatype::decl::plugin* p = u.get_plugin();
-    datatype::def* d = p->mk(n, num_params, params);
+    datatype::decl::plugin& p = u.plugin();
+    datatype::def* d = p.mk(n, num_params, params);
     for (unsigned i = 0; i < num_constructors; ++i) {
         d->add(cs[i]);
     }
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index cb139953b..ae6a1a9ce 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -290,9 +290,11 @@ namespace datatype {
 
     class util {
         ast_manager & m;
-        family_id     m_family_id;
+        mutable family_id     m_family_id;
         mutable decl::plugin* m_plugin;
         typedef std::pair<func_decl*, unsigned> cnstr_depth;
+
+        family_id fid() const;
                 
         obj_map<sort, ptr_vector<func_decl> *>      m_datatype2constructors;
         obj_map<sort, cnstr_depth>                  m_datatype2nonrec_constructor;
@@ -320,7 +322,7 @@ namespace datatype {
         bool is_well_founded(unsigned num_types, sort* const* sorts);
         bool is_covariant(unsigned num_types, sort* const* sorts) const;
         bool is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const;
-        def& get_def(symbol const& s) { return m_plugin->get_def(s); }
+        def& get_def(symbol const& s) { return plugin().get_def(s); }        
         void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;        
 
     public:
@@ -328,23 +330,23 @@ namespace datatype {
         ~util();
         ast_manager & get_manager() const { return m; }
         // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); 
-        bool is_datatype(sort const* s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); }
+        bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }
         bool is_enum_sort(sort* s);
         bool is_recursive(sort * ty);
-        bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
+        bool is_constructor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_CONSTRUCTOR); }
         bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }
-        bool is_recognizer0(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
-        bool is_is(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_IS); }
-        bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
-        bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
-        bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
+        bool is_recognizer0(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_RECOGNISER); }
+        bool is_is(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_IS); }
+        bool is_accessor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_ACCESSOR); }
+        bool is_update_field(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_UPDATE_FIELD); }
+        bool is_constructor(app * f) const { return is_app_of(f, fid(), OP_DT_CONSTRUCTOR); }
         bool is_constructor(expr* e) const { return is_app(e) && is_constructor(to_app(e)); }
-        bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);} 
-        bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);} 
+        bool is_recognizer0(app * f) const { return is_app_of(f, fid(), OP_DT_RECOGNISER);} 
+        bool is_is(app * f) const { return is_app_of(f, fid(), OP_DT_IS);} 
         bool is_is(expr * e) const { return is_app(e) && is_is(to_app(e)); }
         bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
-        bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
-        bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
+        bool is_accessor(app * f) const { return is_app_of(f, fid(), OP_DT_ACCESSOR); }
+        bool is_update_field(app * f) const { return is_app_of(f, fid(), OP_DT_UPDATE_FIELD); }
         app* mk_is(func_decl * c, expr *f);
         ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
         unsigned get_datatype_num_constructors(sort * ty);
@@ -357,8 +359,9 @@ namespace datatype {
         func_decl * get_accessor_constructor(func_decl * accessor);
         func_decl * get_recognizer_constructor(func_decl * recognizer) const;
         func_decl * get_update_accessor(func_decl * update) const;
-        bool has_nested_arrays() const { return m_plugin->has_nested_arrays(); }
-        family_id get_family_id() const { return m_family_id; }
+        bool has_nested_arrays() const { return plugin().has_nested_arrays(); }
+        family_id get_family_id() const { return fid(); }
+        decl::plugin& plugin() const;
         bool are_siblings(sort * s1, sort * s2);
         bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f);
         bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f);
@@ -369,7 +372,6 @@ namespace datatype {
         sort_ref_vector datatype_params(sort * s) const;
         unsigned get_constructor_idx(func_decl * f) const;
         unsigned get_recognizer_constructor_idx(func_decl * f) const;
-        decl::plugin* get_plugin() { return m_plugin; }
         void get_defs(sort* s, ptr_vector<def>& defs);
         def const& get_def(sort* s) const;
         sort_ref mk_list_datatype(sort* elem, symbol const& name,
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index d9e575664..a8e027bb0 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -468,7 +468,7 @@ public:
         solver_ref sNotB = sf(m, p, false /* no proofs */, true, true, symbol::null);
         sA->assert_expr(a);
         sB->assert_expr(b);
-        qe::euf_arith_mbi_plugin pA(sA.get(), sNotA.get());
+        qe::uflia_mbi pA(sA.get(), sNotA.get());
         qe::prop_mbi_plugin pB(sB.get());
         pA.set_shared(vars);
         pB.set_shared(vars);
@@ -518,7 +518,7 @@ public:
         }
         model_ref mdl;
         s->get_model(mdl);
-        qe::euf_arith_mbi_plugin plugin(s.get(), se.get());
+        qe::uflia_mbi plugin(s.get(), se.get());
         plugin.set_shared(vars);
         plugin.project(mdl, lits);
         ctx.regular_stream() << lits << "\n";
diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp
index 2a8528ca3..6469cc35c 100644
--- a/src/opt/opt_parse.cpp
+++ b/src/opt/opt_parse.cpp
@@ -130,7 +130,7 @@ class wcnf {
             if (parsed_lit == 0)
                 break;
             var = abs(parsed_lit);
-            p = m.mk_const(symbol(var), m.mk_bool_sort());
+            p = m.mk_const(symbol((unsigned)var), m.mk_bool_sort());
             if (parsed_lit < 0) p = m.mk_not(p);
             ors.push_back(p);
         }
@@ -198,7 +198,7 @@ class opb {
         }
         app_ref p(m);
         int id = in.parse_int();
-        p = m.mk_const(symbol(id), m.mk_bool_sort());
+        p = m.mk_const(symbol((unsigned)id), m.mk_bool_sort());
         if (negated) p = m.mk_not(p);
         in.skip_whitespace();
         return p;
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index d9084f11b..66d828b94 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -2000,7 +2000,7 @@ namespace smt2 {
             TRACE("skid", tout << "fr->m_skid: " << fr->m_skid << "\n";);
             TRACE("parse_quantifier", tout << "body:\n" << mk_pp(expr_stack().back(), m()) << "\n";);
             if (fr->m_qid == symbol::null)
-                fr->m_qid = symbol(m_scanner.get_line());
+                fr->m_qid = symbol((unsigned)m_scanner.get_line());
             if (fr->m_kind != lambda_k && !m().is_bool(expr_stack().back()))
                 throw parser_exception("quantifier body must be a Boolean expression");
             quantifier* new_q = m().mk_quantifier(fr->m_kind,
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index 9b96a388e..e58f86ba5 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -1092,7 +1092,7 @@ namespace qe {
                 }
                 constructor_decl* constrs[1] = { mk_constructor_decl(symbol("tuple"), symbol("is-tuple"), acc.size(), acc.c_ptr()) };
                 datatype::def* dts = mk_datatype_decl(dt, symbol("tuple"), 0, nullptr, 1, constrs);
-                VERIFY(dt.get_plugin()->mk_datatypes(1, &dts, 0, nullptr, srts));
+                VERIFY(dt.plugin().mk_datatypes(1, &dts, 0, nullptr, srts));
                 del_datatype_decl(dts);
                 sort* tuple = srts.get(0);
                 ptr_vector<func_decl> const & decls = *dt.get_datatype_constructors(tuple);
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 71a783c4f..f6ccf7b7d 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -58,6 +58,29 @@ namespace qe {
         }
     }
 
+    bool mbi_plugin::is_shared(func_decl* f) {
+        return f->get_family_id() != null_family_id || m_shared.contains(f);
+    }
+
+    bool mbi_plugin::is_shared(expr* e) {
+        e = m_rep ? m_rep(e) : e;
+        if (!is_app(e)) return false;
+        unsigned id = e->get_id();
+        m_is_shared.reserve(id + 1, l_undef);
+        lbool r = m_is_shared[id];
+        if (r != l_undef) return r == l_true;
+        app* a = to_app(e);
+        bool all_shared = is_shared(a->get_decl());
+        for (expr* arg : *a) {
+            if (!all_shared)
+                break;
+            if (!is_shared(arg)) 
+                all_shared = false;
+        }
+        m_is_shared[id] = all_shared ? l_true : l_false;
+        return all_shared;
+    }
+
 
     // -------------------------------
     // prop_mbi
@@ -78,7 +101,7 @@ namespace qe {
             lits.reset();
             for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) {
                 func_decl* c = mdl->get_constant(i);
-                if (m_shared.contains(c)) {
+                if (is_shared(c)) {
                     if (m.is_true(mdl->get_const_interp(c))) {
                         lits.push_back(m.mk_const(c));
                     }
@@ -98,9 +121,9 @@ namespace qe {
     }
 
     // -------------------------------
-    // euf_arith_mbi
+    // uflia_mbi
 
-    struct euf_arith_mbi_plugin::is_atom_proc {
+    struct uflia_mbi::is_atom_proc {
         ast_manager&         m;
         expr_ref_vector&     m_atoms;
         obj_hashtable<expr>& m_atom_set;
@@ -124,56 +147,7 @@ namespace qe {
         void operator()(expr*) {}
     };
 
-    struct euf_arith_mbi_plugin::is_arith_var_proc {
-        ast_manager&    m;
-        app_ref_vector& m_avars;
-        app_ref_vector& m_proxies;
-        arith_util      m_arith;
-        obj_hashtable<expr> m_seen;
-        is_arith_var_proc(app_ref_vector& avars, app_ref_vector& proxies):
-            m(avars.m()), m_avars(avars), m_proxies(proxies), m_arith(m) {
-        }
-        void operator()(app* a) {
-            if (is_arith_op(a) || a->get_family_id() == m.get_basic_family_id()) {
-                return;
-            }
-
-            if (m_arith.is_int_real(a)) {
-                m_avars.push_back(a);
-                if (!m_seen.contains(a)) {
-                    m_proxies.push_back(a);
-                    m_seen.insert(a);
-                }
-            }
-            for (expr* arg : *a) {
-                if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) {
-                    m_proxies.push_back(to_app(arg));
-                    m_seen.insert(arg);
-                }
-            }
-        }
-        bool is_arith_op(app* a) {
-            return a->get_family_id() == m_arith.get_family_id();
-        }
-        void operator()(expr*) {}
-    };
-
-    void euf_arith_mbi_plugin::filter_private_arith(app_ref_vector& avars) {
-        arith_util a(m);
-        unsigned j = 0;
-        obj_hashtable<func_decl> shared;
-        for (func_decl* f : m_shared) shared.insert(f);
-        for (unsigned i = 0; i < avars.size(); ++i) {
-            app* v = avars.get(i);
-            if (!shared.contains(v->get_decl()) && 
-                v->get_family_id() != a.get_family_id()) {
-                avars[j++] = v;
-            }
-        }
-        avars.shrink(j);
-    }
-
-    euf_arith_mbi_plugin::euf_arith_mbi_plugin(solver* s, solver* sNot):
+    uflia_mbi::uflia_mbi(solver* s, solver* sNot):
         mbi_plugin(s->get_manager()),
         m_atoms(m),
         m_fmls(m),
@@ -187,7 +161,7 @@ namespace qe {
         collect_atoms(m_fmls);
     }
 
-    void euf_arith_mbi_plugin::collect_atoms(expr_ref_vector const& fmls) {
+    void uflia_mbi::collect_atoms(expr_ref_vector const& fmls) {
         expr_fast_mark1 marks;
         is_atom_proc proc(m_atoms, m_atom_set);
         for (expr* e : fmls) {
@@ -195,7 +169,7 @@ namespace qe {
         }
     }
 
-    bool euf_arith_mbi_plugin::get_literals(model_ref& mdl, expr_ref_vector& lits) {
+    bool uflia_mbi::get_literals(model_ref& mdl, expr_ref_vector& lits) {
         lits.reset();
         for (expr* e : m_atoms) {
             if (mdl->is_true(e)) {
@@ -223,16 +197,41 @@ namespace qe {
 
 
     /** 
-     * \brief extract arithmetical variables and arithmetical terms in shared positions.
+     * \brief A subterm is an arithmetic variable if:
+     *  1. it is not shared.
+     *  2. it occurs under an arithmetic operation.
+     *  3. it is not an arithmetic expression.
+     * 
+     *  The result is ordered using deepest term first.
      */
-    app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies) {
+    app_ref_vector uflia_mbi::get_arith_vars(expr_ref_vector& lits) {
         app_ref_vector avars(m); 
-        is_arith_var_proc _proc(avars, proxies);
-        for_each_expr(_proc, lits);
+        svector<bool> seen;
+        arith_util a(m);
+        for (expr* e : subterms(lits)) {
+            if ((m.is_eq(e) && a.is_int_real(to_app(e)->get_arg(0))) || a.is_arith_expr(e)) {
+                for (expr* arg : *to_app(e)) {
+                    unsigned id = arg->get_id();
+                    seen.reserve(id + 1, false);
+                    if (is_app(arg) && !m.is_eq(arg) && !a.is_arith_expr(arg) && !is_shared(arg) && !seen[id]) {
+                        seen[id] = true;
+                        avars.push_back(to_app(arg));
+                    }
+                }
+            }
+        }
+        order_avars(avars);
+        TRACE("qe", tout << "vars: " << avars << "\n";);
         return avars;
     }
 
-    mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) {
+    vector<def> uflia_mbi::arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits) {
+        arith_project_plugin ap(m);
+        ap.set_check_purified(false);
+        return ap.project(*mdl.get(), avars, lits);
+    }
+
+    mbi_result uflia_mbi::operator()(expr_ref_vector& lits, model_ref& mdl) {
         lbool r = m_solver->check_sat(lits);
 
         switch (r) {
@@ -259,169 +258,83 @@ namespace qe {
         }
     }
 
-    void euf_arith_mbi_plugin::project(model_ref& mdl, expr_ref_vector& lits) {
-        TRACE("qe", tout << lits << "\n" << *mdl << "\n";);
-        TRACE("qe", tout << m_solver->get_assertions() << "\n";);
+    /**
+       \brief main projection routine
+    */
+    void uflia_mbi::project(model_ref& mdl, expr_ref_vector& lits) {
+        TRACE("qe", 
+              tout << lits << "\n" << *mdl << "\n";
+              tout << m_solver->get_assertions() << "\n";);
 
-        // 0. saturation
-        array_project_plugin arp(m);
-        arp.saturate(*mdl, m_shared, lits);
-
-        // . arithmetical variables - atomic and in purified positions
-        app_ref_vector proxies(m);
-        app_ref_vector avars = get_arith_vars(mdl, lits, proxies);
-        TRACE("qe", tout << "vars: " << avars << "\nproxies: " << proxies << "\nlits: " << lits << "\n";);
-
-        // . project private non-arithmetical variables from lits
-        project_euf(mdl, lits, avars);
-
-        // . Minimzie span between smallest and largest proxy variable.
-        minimize_span(mdl, avars, proxies);
-
-        // . Order arithmetical variables and purified positions
-        order_avars(mdl, lits, avars, proxies);
-        TRACE("qe", tout << "ordered: " << lits << "\n";);
-
-        // . Perform arithmetical projection
-        arith_project_plugin ap(m);
-        ap.set_check_purified(false);
-        auto defs = ap.project(*mdl.get(), avars, lits);
-        TRACE("qe", tout << "aproject: " << lits << "\n";);
-
-        // . Substitute solution into lits
+        add_dcert(mdl, lits);
+        auto avars = get_arith_vars(lits);
+        auto defs = arith_project(mdl, avars, lits);
         substitute(defs, lits);
-        TRACE("qe", tout << "substitute: " << lits << "\n";);
-        IF_VERBOSE(1, verbose_stream() << lits << "\n");
+        project_euf(mdl, lits);
+    }
+
+    /**
+       \brief add difference certificates to formula.
+       
+       First version just uses an Ackerman reduction.
+
+       It should be replaced by DCert.
+    */
+    void uflia_mbi::add_dcert(model_ref& mdl, expr_ref_vector& lits) {        
+        term_graph tg(m);
+        func_decl_ref_vector shared(m_shared_trail);
+        tg.set_vars(shared, false);
+        tg.add_lits(lits);
+        lits.append(tg.get_ackerman_disequalities());
+        TRACE("qe", tout << "project: " << lits << "\n";);                
     }
 
     /**
      * \brief substitute solution to arithmetical variables into lits
      */
-    void euf_arith_mbi_plugin::substitute(vector<def> const& defs, expr_ref_vector& lits) {
+    void uflia_mbi::substitute(vector<def> const& defs, expr_ref_vector& lits) {
         for (auto const& def : defs) {
             expr_safe_replace rep(m);
             rep.insert(def.var, def.term);
             rep(lits);
         }
+        TRACE("qe", tout << "substitute: " << lits << "\n";);
+        IF_VERBOSE(1, verbose_stream() << lits << "\n");
     }
 
     /**
      * \brief project private symbols.
-     * - project with respect to shared symbols only.
-     *   retains equalities that are independent of arithmetic
-     * - project with respect to shared + arithmetic basic terms
-     *   retains predicates that are projected by arithmetic 
      */
-    void euf_arith_mbi_plugin::project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) {
-        term_graph tg1(m), tg2(m);
-        func_decl_ref_vector shared(m_shared);
-        tg1.set_vars(shared, false);
-        for (app* a : avars) shared.push_back(a->get_decl());
-        tg2.set_vars(shared, false);
-        tg1.add_lits(lits);
-        tg2.add_lits(lits);
+    void uflia_mbi::project_euf(model_ref& mdl, expr_ref_vector& lits) {
+        term_graph tg(m);
+        func_decl_ref_vector shared(m_shared_trail);
+        tg.set_vars(shared, false);
+        tg.add_lits(lits);
         lits.reset();
-        lits.append(tg1.project(*mdl.get()));
-        lits.append(tg2.project(*mdl.get()));
+        lits.append(tg.project(*mdl.get()));
         TRACE("qe", tout << "project: " << lits << "\n";);                
     }
 
-    vector<std::pair<rational, app*>> euf_arith_mbi_plugin::sort_proxies(model_ref& mdl, app_ref_vector const& proxies) {
-        arith_util a(m);
-        model_evaluator mev(*mdl.get());
-        vector<std::pair<rational, app*>> vals;
-        for (app* v : proxies) {
-            rational val;
-            expr_ref tmp = mev(v);
-            VERIFY(a.is_numeral(tmp, val));
-            vals.push_back(std::make_pair(val, v));
-        }
-        struct compare_first {
-            bool operator()(std::pair<rational, app*> const& x,
-                          std::pair<rational, app*> const& y) const {
-                return x.first < y.first;
-            }
-        };
-        // add offset ordering between proxies
-        compare_first cmp;
-        std::sort(vals.begin(), vals.end(), cmp);
-        return vals;
-    }
-
-    void euf_arith_mbi_plugin::minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies) {
-#if 0
-        arith_util a(m);
-        opt::context opt(m);        
-        expr_ref_vector fmls(m);
-        m_solver->get_assertions(fmls);
-        for (expr* l : fmls) opt.add_hard_constraint(l);
-        vector<std::pair<rational, app*>> vals = sort_proxies(mdl, proxies);
-        app_ref t(m);
-        for (unsigned i = 1; i < vals.size(); ++i) {
-            rational offset = vals[i].first - vals[i-1].first;
-            expr* t1 = vals[i-1].second;
-            expr* t2 = vals[i].second;
-            if (offset.is_zero()) {
-                t = m.mk_eq(t1, t2);
-            }
-            else {
-                SASSERT(offset.is_pos());
-                t = a.mk_lt(t1, t2);
-            }
-            opt.add_hard_constraint(t);
-        }
-        t = a.mk_sub(vals[0].second, vals.back().second);
-        opt.add_objective(t, true);
-        expr_ref_vector asms(m);
-        VERIFY(l_true == opt.optimize(asms));
-        opt.get_model(mdl);
-        model_evaluator mev(*mdl.get());
-        std::cout << mev(t) << "\n";
-#endif
-    }
-
     /**
      * \brief Order arithmetical variables:
-     * 1. add literals that order the proxies according to the model.
-     * 2. sort arithmetical terms, such that deepest terms are first.
+     * sort arithmetical terms, such that deepest terms are first.
      */
-    void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) {
-        arith_util a(m);
-        model_evaluator mev(*mdl.get());
-        vector<std::pair<rational, app*>> vals = sort_proxies(mdl, proxies);
-        for (unsigned i = 1; i < vals.size(); ++i) {
-            rational offset = vals[i].first - vals[i-1].first;
-            expr* t1 = vals[i-1].second;
-            expr* t2 = vals[i].second;
-            if (offset.is_zero()) {
-                lits.push_back(m.mk_eq(t1, t2));
-            }
-            else {
-                expr_ref t(a.mk_add(t1, a.mk_numeral(offset, true)), m);
-                lits.push_back(a.mk_le(t, t2));
-            }
-        }
-
-        // filter out only private variables
-        filter_private_arith(avars);
+    void uflia_mbi::order_avars(app_ref_vector& avars) {
 
         // sort avars based on depth
-        struct compare_depth {
-            bool operator()(app* x, app* y) const {
+        std::function<bool(app*, app*)> compare_depth = 
+            [](app* x, app* y) {
                 return 
                     (x->get_depth() > y->get_depth()) || 
                     (x->get_depth() == y->get_depth() && x->get_id() > y->get_id());
-            }
         };
-        compare_depth cmpd;
-        std::sort(avars.c_ptr(), avars.c_ptr() + avars.size(), cmpd);
-        TRACE("qe", tout << lits << "\navars:" << avars << "\n" << *mdl << "\n";);
+        std::sort(avars.c_ptr(), avars.c_ptr() + avars.size(), compare_depth);
+        TRACE("qe", tout << "avars:" << avars << "\n";);
     }
 
-    void euf_arith_mbi_plugin::block(expr_ref_vector const& lits) {
+    void uflia_mbi::block(expr_ref_vector const& lits) {
         // want to rely only on atoms from original literals: collect_atoms(lits);
         expr_ref conj(mk_not(mk_and(lits)), m);
-        //m_fmls.push_back(conj);
         TRACE("qe", tout << "block " << lits << "\n";);
         m_solver->assert_expr(conj);
     }
@@ -512,83 +425,4 @@ namespace qe {
         }
     }
 
-    lbool interpolator::vurtego(mbi_plugin& a, mbi_plugin& b, expr_ref& itp, model_ref &mdl) {
-        /**
-           Assumptions on mbi_plugin()
-           Let local be assertions local to the plugin
-           Let blocked be clauses added by blocked, kept separately from local
-           mbi_plugin::check(lits, mdl, bool force_model):
-              if lits.empty()  and mdl == nullptr then
-                  if is_sat(local & blocked) then
-                      return l_true, mbp of local, mdl of local & blocked
-                  else
-                      return l_false
-              else if !lits.empty() then
-                  if is_sat(local & mdl & blocked)
-                      return l_true, lits, extension of mdl to local
-                  else if is_sat(local & lits & blocked)
-                      if (force_model) then
-                        return l_false, core of model, nullptr
-                      else
-                        return l_true, mbp of local, mdl of local & blocked
-                  else if !is_sat(local & lits) then
-                      return l_false, mbp of local, nullptr
-                  else if is_sat(local & lits) && !is_sat(local & lits & blocked)
-                      MISSING CASE
-                      MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked
-                      in this case !is_sat(local & lits & mdl) and is_sat(mdl, blocked)
-                          let mdl_blocked be lits of blocked that are true in mdl
-                          return l_false, core of lits & mdl_blocked, nullptr
-
-           mbi_plugin::block(phi): add phi to blocked
-
-           probably should use the operator() instead of check.
-           mbi_augment -- means consistent with lits but not with the mdl
-           mbi_sat -- means consistent with lits and mdl
-
-         */
-        expr_ref_vector lits(m), itps(m);
-        while (true) {
-            // when lits.empty(), this picks an A-implicant consistent with B
-            // when !lits.empty(), checks whether mdl of shared vocab extends to A
-            bool force_model = !lits.empty();
-            switch (a.check_ag(lits, mdl, force_model)) {
-            case l_true:
-                if (force_model)
-                    // mdl is a model for a && b
-                    return l_true;
-                switch (b.check_ag(lits, mdl, false)) {
-                case l_true:
-                    /* can return true if know that b did not change
-                       the model. For now, cycle back to A.  */
-                    SASSERT(!lits.empty());
-                    SASSERT(mdl);
-                    break;
-                case l_false:
-                    // Force a different A-implicant
-                    a.block(lits);
-                    lits.reset();
-                    mdl.reset();
-                    break;
-                case l_undef:
-                    return l_undef;
-                }
-            case l_false:
-                if (lits.empty()) {
-                    // no more A-implicants, terminate
-                    itp = mk_and(itps);
-                    return l_false;
-                }
-                // force B to pick a different model or a different implicant
-                b.block(lits);
-                itps.push_back(mk_not(mk_and(lits)));
-                lits.reset();
-                mdl.reset();
-                break;
-            case l_undef:
-                return l_undef;
-            }
-        }
-    }
-
 };
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index 0458bd8e0..a693bf493 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -33,19 +33,38 @@ namespace qe {
     class mbi_plugin {
     protected:
         ast_manager& m;
-        func_decl_ref_vector m_shared;
+        func_decl_ref_vector     m_shared_trail;
+        obj_hashtable<func_decl> m_shared;
+        svector<lbool>           m_is_shared;
+        std::function<expr*(expr*)> m_rep;
+
+        lbool is_shared_cached(expr* e);
     public:
-        mbi_plugin(ast_manager& m): m(m), m_shared(m) {}
+        mbi_plugin(ast_manager& m): m(m), m_shared_trail(m) {}
         virtual ~mbi_plugin() {}
 
         /**
          * Set the shared symbols.
          */
-        virtual void set_shared(func_decl_ref_vector const& vars) {
+        void set_shared(func_decl_ref_vector const& vars) {
+            m_shared_trail.reset();
             m_shared.reset();
-            m_shared.append(vars);
+            m_is_shared.reset();
+            m_shared_trail.append(vars);
+            for (auto* f : vars) m_shared.insert(f);
         }
 
+        /**
+         * Set representative (shared) expression finder.
+         */
+        void set_rep(std::function<expr*(expr*)>& rep) { m_rep = rep; }
+
+        /**
+         * determine whether expression/function is shared.
+         */
+        bool is_shared(expr* e);
+        bool is_shared(func_decl* f);
+
         /**
          * \brief Utility that works modulo a background state.
          * - vars
@@ -77,11 +96,6 @@ namespace qe {
          */
         lbool check(expr_ref_vector& lits, model_ref& mdl);
 
-        virtual lbool check_ag(expr_ref_vector& lits, model_ref& mdl, bool force_model) {
-            return l_undef;
-        }
-
-
     };
 
     class prop_mbi_plugin : public mbi_plugin {
@@ -93,28 +107,26 @@ namespace qe {
         void block(expr_ref_vector const& lits) override;
     };
 
-
-    class euf_arith_mbi_plugin : public mbi_plugin {
+    class uflia_mbi : public mbi_plugin {
         expr_ref_vector     m_atoms;
         obj_hashtable<expr> m_atom_set;
         expr_ref_vector     m_fmls;
         solver_ref          m_solver;
         solver_ref          m_dual_solver;
         struct is_atom_proc;
-        struct is_arith_var_proc;
 
-        app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies);
         bool get_literals(model_ref& mdl, expr_ref_vector& lits);
         void collect_atoms(expr_ref_vector const& fmls);
-        void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
-        vector<std::pair<rational, app*>> sort_proxies(model_ref& mdl, app_ref_vector const& proxies);
-        void minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies);
-        void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies);
+        void order_avars(app_ref_vector& avars);
+
+        void add_dcert(model_ref& mdl, expr_ref_vector& lits);
+        app_ref_vector get_arith_vars(expr_ref_vector& lits);
+        vector<def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
         void substitute(vector<def> const& defs, expr_ref_vector& lits);
-        void filter_private_arith(app_ref_vector& avars);
+        void project_euf(model_ref& mdl, expr_ref_vector& lits);
     public:
-        euf_arith_mbi_plugin(solver* s, solver* emptySolver);
-        ~euf_arith_mbi_plugin() override {}
+        uflia_mbi(solver* s, solver* emptySolver);
+        ~uflia_mbi() override {}
         mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
         void project(model_ref& mdl, expr_ref_vector& lits);
         void block(expr_ref_vector const& lits) override;
@@ -129,7 +141,6 @@ namespace qe {
         interpolator(ast_manager& m):m(m) {}
         lbool pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
         lbool pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
-        lbool vurtego(mbi_plugin &a, mbi_plugin &b, expr_ref &itp, model_ref &mdl);
     };
 
 };
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index 166b18bc9..dd631f228 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -584,7 +584,6 @@ namespace qe {
         u_map<expr*> m_term2app;
         u_map<expr*> m_root2rep;
 
-
         model_ref m_model;
         expr_ref_vector m_pinned;  // tracks expr in the maps
 
@@ -1183,4 +1182,50 @@ namespace qe {
         SASSERT(t && "only get representatives");
         return m_projector->find_term2app(*t);
     }
+
+    expr_ref_vector term_graph::dcert(model& mdl, expr_ref_vector const& lits) {
+#if 0
+        obj_pair_hashtable<expr, expr> diseqs;
+        extract_disequalities(lits, diseqs);
+        svector<std::pair<expr*, expr*>> todo;
+        for (auto const& p : diseqs) todo.push_back(p);
+        expr_ref_vector result(m);
+
+        // make sure that diseqs is closed under function applications
+        // of uninterpreted functions.
+        for (unsigned idx = 0; idx < todo.size(); ++idx) {
+            auto p = todo[idx];
+            for (app* t1 : partition_of(p.first)) {
+                for (app* t2 : partition_of(p.second)) {
+                    if (same_function(t1, t2)) {
+                        unsigned sz = t1->get_num_args();
+                        bool found = false;
+                        std::pair<expr*, expr*> q(nullptr, nullptr);
+                        for (unsigned i = 0; i < sz; ++i) {
+                            expr* arg1 = t1->get_arg(i);
+                            expr* arg2 = t2->get_arg(i);
+                            if (mdl(arg1) == mdl(t2)) {
+                                continue;
+                            }
+                            if (in_table(diseqs, arg1, arg2)) {
+                                found = true;
+                                break;
+                            }
+                            q = make_diseq(arg1, arg2);
+                        }
+                        if (!found) {
+                            diseqs.insert(q);
+                            todo.push_back(q);
+                            result.push_back(m.mk_not(m.mk_eq(q.first, q.second)));
+                        }
+                    }
+                }
+            }
+        }
+        return result;
+#endif
+        NOT_IMPLEMENTED_YET();
+        return expr_ref_vector(m);
+    }
+
 }
diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h
index ef12ab683..6b0e1c437 100644
--- a/src/qe/qe_term_graph.h
+++ b/src/qe/qe_term_graph.h
@@ -123,6 +123,16 @@ namespace qe {
          */
         expr_ref_vector get_ackerman_disequalities();
 
+        /**
+         * Produce model-based disequality 
+         * certificate corresponding to 
+         * definition in BGVS 2020.
+         * A disequality certificate is a reduced set of 
+         * disequalities, true under mdl, such that the literals
+         * can be satisfied when non-shared symbols are projected.
+         */
+        expr_ref_vector dcert(model& mdl, expr_ref_vector const& lits);
+
         /**
          * Produce a model-based partition.
          */
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index b2137795b..c14e46578 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -157,13 +157,15 @@ class sat_tactic : public tactic {
     imp *      m_imp;
     params_ref m_params;
     statistics m_stats;
+    symbol     m_xor_solver;
 
 public:
     sat_tactic(ast_manager & m, params_ref const & p):
         m_imp(nullptr),
-        m_params(p) {
+        m_params(p),
+        m_xor_solver("xor_solver") {
         sat_params p1(p);
-        m_params.set_bool("xor_solver", p1.xor_solver());
+        m_params.set_bool(m_xor_solver, p1.xor_solver());
     }
 
     tactic * translate(ast_manager & m) override {
@@ -177,7 +179,7 @@ public:
     void updt_params(params_ref const & p) override {
         m_params = p;
         sat_params p1(p);
-        m_params.set_bool("xor_solver", p1.xor_solver());
+        m_params.set_bool(m_xor_solver, p1.xor_solver());
         if (m_imp) m_imp->updt_params(p);
     }
 
diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp
index a57b0299f..6b937d8f2 100644
--- a/src/smt/expr_context_simplifier.cpp
+++ b/src/smt/expr_context_simplifier.cpp
@@ -315,7 +315,7 @@ bool expr_context_simplifier::is_false(expr* e) const {
 expr_strong_context_simplifier::expr_strong_context_simplifier(smt_params& p, ast_manager& m): 
     m_manager(m), m_arith(m), m_fn(nullptr,m), m_solver(m, p) {
     sort* i_sort = m_arith.mk_int();
-    m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
+    m_fn = m.mk_func_decl(symbol(0xbeef101u), i_sort, m.mk_bool_sort());
 }
 
 
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index 06688b7bb..0f4f1e0fc 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -40,7 +40,7 @@ public:
         m(m), m_params(p), m_solver(m, m_front_p),  
         m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0) {
         sort* i_sort = m_arith.mk_int();
-        m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
+        m_fn = m.mk_func_decl(symbol(0xbeef101u), i_sort, m.mk_bool_sort());
     }
 
     tactic * translate(ast_manager & m) override {
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index b4bcfa146..2d558e29e 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -173,7 +173,7 @@ namespace smt {
         for (unsigned i = 0; i < n->get_num_args(); ++i) {
             bindings.push_back(n->get_arg(i)->get_owner());
         }
-        unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0;
+        unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.plugin().get_axiom_base_id(d->get_name()) : 0;
         unsigned i = 0;
         for (func_decl * acc : accessors) {
             app_ref acc_app(m.mk_app(acc, n->get_owner()), m);
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 40c6b6b87..c8922475c 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -2202,7 +2202,7 @@ namespace smt {
 
     app_ref theory_pb::literal2expr(literal lit) {
         ast_manager& m = get_manager();
-        app_ref arg(m.mk_const(symbol(lit.var()), m.mk_bool_sort()), m);                
+        app_ref arg(m.mk_const(symbol((unsigned)lit.var()), m.mk_bool_sort()), m);                
         return app_ref(lit.sign() ? m.mk_not(arg) : arg, m);
     }
 
diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp
index e44c92f30..e0827ba28 100644
--- a/src/test/dl_context.cpp
+++ b/src/test/dl_context.cpp
@@ -4,9 +4,10 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#include "muz/fp/datalog_parser.h"
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"
+#include "ast/reg_decl_plugins.h"
+#include "muz/fp/datalog_parser.h"
 #include "muz/base/dl_context.h"
 #include "smt/params/smt_params.h"
 #include "muz/fp/dl_register_engine.h"
@@ -62,6 +63,7 @@ static lbool dl_context_eval_unary_predicate(ast_manager & m, context & ctx, cha
 
 static void dl_context_simple_query_test(params_ref & params) {
     ast_manager m;
+    reg_decl_plugins(m);
     dl_decl_util decl_util(m);
     register_engine re;
     smt_params fparams;
diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp
index 7cbbde450..352748087 100644
--- a/src/test/dl_product_relation.cpp
+++ b/src/test/dl_product_relation.cpp
@@ -5,6 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #ifdef _WINDOWS
+#include "ast/reg_decl_plugins.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"
 #include "muz/rel/dl_finite_product_relation.h"
@@ -29,6 +30,7 @@ namespace datalog {
 
     void test_functional_columns(smt_params fparams, params_ref& params) {
         ast_manager m;
+        reg_decl_plugins(m);
         register_engine re;
         context ctx(m, re, fparams);
         rel_context_base& rctx = *ctx.get_rel_context();
@@ -133,6 +135,7 @@ namespace datalog {
 
     void test_finite_product_relation(smt_params fparams, params_ref& params) {
         ast_manager m;
+        reg_decl_plugins(m);
         register_engine re;
         context ctx(m, re, fparams);
         ctx.updt_params(params);
diff --git a/src/test/dl_relation.cpp b/src/test/dl_relation.cpp
index 3abd60ce2..1940de3e9 100644
--- a/src/test/dl_relation.cpp
+++ b/src/test/dl_relation.cpp
@@ -5,6 +5,8 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 #ifdef _WINDOWS
+
+#include "ast/reg_decl_plugins.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"
 #include "muz/rel/dl_relation_manager.h"
@@ -18,6 +20,7 @@ namespace datalog {
     static void test_interval_relation() {
         smt_params params;
         ast_manager ast_m;
+        reg_decl_plugins(ast_m);
         register_engine re;
         context ctx(ast_m, re, params);    
         arith_util autil(ast_m);
@@ -122,6 +125,7 @@ namespace datalog {
 
         smt_params params;
         ast_manager ast_m;
+        reg_decl_plugins(ast_m);
         register_engine re;
         context ctx(ast_m, re, params);    
         arith_util autil(ast_m);
diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp
index 8eb864f7b..b3082cc6a 100644
--- a/src/test/dl_table.cpp
+++ b/src/test/dl_table.cpp
@@ -1,6 +1,7 @@
 /*++
 Copyright (c) 2015 Microsoft Corporation
 --*/
+#include "ast/reg_decl_plugins.h"
 #include "muz/base/dl_context.h"
 #include "muz/rel/dl_table.h"
 #include "muz/fp/dl_register_engine.h"
@@ -22,6 +23,7 @@ static void test_table(mk_table_fn mk_table) {
     sig.push_back(4);
     smt_params params;
     ast_manager ast_m;
+    reg_decl_plugins(ast_m);
     datalog::register_engine re;
     datalog::context ctx(ast_m, re, params);    
     datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager();
diff --git a/src/test/theory_dl.cpp b/src/test/theory_dl.cpp
index 9a28f3653..5b11069aa 100644
--- a/src/test/theory_dl.cpp
+++ b/src/test/theory_dl.cpp
@@ -4,14 +4,16 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#include "smt/smt_context.h"
 #include "ast/dl_decl_plugin.h"
-#include "ast/ast_pp.h"
-#include "model/model_v2_pp.h"
 #include "ast/reg_decl_plugins.h"
+#include "ast/ast_pp.h"
+#include "ast/reg_decl_plugins.h"
+#include "smt/smt_context.h"
+#include "model/model_v2_pp.h"
 
 void tst_theory_dl() {
     ast_manager m;
+    reg_decl_plugins(m);
     smt_params params;
     params.m_model = true;
     datalog::dl_decl_util u(m);