diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 1aeecdaac..72e843227 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -297,11 +297,11 @@ public:
     bool is_power0(expr const * n) const { return is_app_of(n, m_afid, OP_POWER0); }
 
     bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
-    bool is_int(expr const * n) const { return is_int(get_sort(n)); }
+    bool is_int(expr const * n) const { return is_int(n->get_sort()); }
     bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
-    bool is_real(expr const * n) const { return is_real(get_sort(n)); }
+    bool is_real(expr const * n) const { return is_real(n->get_sort()); }
     bool is_int_real(sort const * s) const { return s->get_family_id() == m_afid; }
-    bool is_int_real(expr const * n) const { return is_int_real(get_sort(n)); }
+    bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); }
 
     bool is_sin(expr const* n) const { return is_app_of(n, m_afid, OP_SIN); }
     bool is_cos(expr const* n) const { return is_app_of(n, m_afid, OP_COS); }
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 76a88660c..529df32fa 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -144,7 +144,7 @@ public:
     array_recognizers(family_id fid):m_fid(fid) {}
     family_id get_family_id() const { return m_fid; }
     bool is_array(sort* s) const { return is_sort_of(s, m_fid, ARRAY_SORT);}
-    bool is_array(expr* n) const { return is_array(get_sort(n)); }
+    bool is_array(expr* n) const { return is_array(n->get_sort()); }
     bool is_select(expr* n) const { return is_app_of(n, m_fid, OP_SELECT); }
     bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); }
     bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 36d44457c..fcdaac5a0 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -420,14 +420,14 @@ quantifier::quantifier(unsigned num_decls, sort * const * decl_sorts, symbol con
 //
 // -----------------------------------
 
-sort * get_sort(expr const * n) {
-    switch(n->get_kind()) {
+sort* expr::get_sort() const {
+    switch (get_kind()) {
     case AST_APP:
-        return to_app(n)->get_decl()->get_range();
+        return to_app(this)->get_decl()->get_range();
     case AST_VAR:
-        return to_var(n)->get_sort();
+        return to_var(this)->_get_sort();
     case AST_QUANTIFIER:
-        return to_quantifier(n)->get_sort();
+        return to_quantifier(this)->_get_sort();
     default:
         UNREACHABLE();
         return nullptr;
@@ -2513,7 +2513,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
     sort* s = nullptr;
     if (k == lambda_k) {
         array_util autil(*this);
-        s = autil.mk_array_sort(num_decls, decl_sorts, ::get_sort(body));
+        s = autil.mk_array_sort(num_decls, decl_sorts, body->get_sort());
     }
     else {
         s = mk_bool_sort();
@@ -2541,7 +2541,7 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort
     unsigned sz               = quantifier::get_obj_size(num_decls, 0, 0);
     void * mem                = allocate_node(sz);
     array_util autil(*this);
-    sort* s = autil.mk_array_sort(num_decls, decl_sorts, ::get_sort(body));
+    sort* s = autil.mk_array_sort(num_decls, decl_sorts, body->get_sort());
     quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s);
     quantifier * r = register_node(new_node);
     if (m_trace_stream && r == new_node) {
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 38b7280fd..ab70f6694 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -668,6 +668,8 @@ protected:
 
     expr(ast_kind k):ast(k) {}
 public:
+
+    sort* get_sort() const;
 };
 
 // -----------------------------------
@@ -719,6 +721,7 @@ public:
     unsigned get_size() const { return get_obj_size(get_num_args()); }
     expr * const * begin() const { return m_args; }
     expr * const * end() const { return m_args + m_num_args; }
+    sort * _get_sort() const { return get_decl()->get_range(); }
 
     unsigned get_depth() const { return flags()->m_depth; }
     bool is_ground() const { return flags()->m_ground; }
@@ -807,7 +810,7 @@ class var : public expr {
     var(unsigned idx, sort * s):expr(AST_VAR), m_idx(idx), m_sort(s) {}
 public:
     unsigned get_idx() const { return m_idx; }
-    sort * get_sort() const { return m_sort; }
+    sort * _get_sort() const { return m_sort; }
     unsigned get_size() const { return get_obj_size(); }
 };
 
@@ -863,7 +866,7 @@ public:
     symbol const & get_decl_name(unsigned idx) const { return get_decl_names()[idx]; }
     expr * get_expr() const { return m_expr; }
 
-    sort * get_sort() const { return m_sort; }
+    sort * _get_sort() const { return m_sort; }
 
     unsigned get_depth() const { return m_depth; }
 
@@ -1391,14 +1394,13 @@ inline bool has_labels(expr const * n) {
     else return false;
 }
 
-sort * get_sort(expr const * n);
 
 class basic_recognizers {
     family_id m_fid;
 public:
     basic_recognizers(family_id fid):m_fid(fid) {}
     bool is_bool(sort const * s) const { return is_sort_of(s, m_fid, BOOL_SORT); }
-    bool is_bool(expr const * n) const { return is_bool(get_sort(n)); }
+    bool is_bool(expr const * n) const { return is_bool(n->get_sort()); }
     bool is_or(expr const * n) const { return is_app_of(n, m_fid, OP_OR); }
     bool is_implies(expr const * n) const { return is_app_of(n, m_fid, OP_IMPLIES); }
     bool is_and(expr const * n) const { return is_app_of(n, m_fid, OP_AND); }
@@ -1733,7 +1735,7 @@ protected:
     }
 
 public:
-    sort * get_sort(expr const * n) const { return ::get_sort(n); }
+    sort * get_sort(expr const * n) const { return n->get_sort(); }
     void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const;
     void check_sorts_core(ast const * n) const;
     bool check_sorts(ast const * n) const;
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index f8d2e9e70..98a34a376 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -300,7 +300,7 @@ public:
     bool is_zero(expr const * e) const;
     bool is_one(expr const* e) const;
     bool is_bv_sort(sort const * s) const;
-    bool is_bv(expr const* e) const {  return is_bv_sort(get_sort(e)); }
+    bool is_bv(expr const* e) const {  return is_bv_sort(e->get_sort()); }
 
     bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
     bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index a8edb2dcc..456ce45eb 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -43,6 +43,8 @@ struct enum2bv_rewriter::imp {
         ast_manager&         m;        
         datatype_util        m_dt;
         bv_util              m_bv;
+        bool                 m_enable_unate { false };
+        unsigned             m_unate_bound { 30 };
 
         rw_cfg(imp& i, ast_manager & m) :
             m_imp(i),
@@ -51,6 +53,38 @@ struct enum2bv_rewriter::imp {
             m_bv(m)
         {}
 
+        bool is_unate(sort* s) {
+            if (!m_enable_unate)
+                return false;
+            unsigned nc = m_dt.get_datatype_num_constructors(s);
+            return 1 < nc && nc <= m_unate_bound;            
+        }
+
+        expr* value2bv(unsigned idx, sort* s) {
+            unsigned bv_size = get_bv_size(s);
+            sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
+            if (is_unate(s))
+                return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort);
+            else 
+                return m_bv.mk_numeral(rational(idx), bv_sort);
+        }
+
+        void constrain_domain(expr* x, sort* s, sort* bv_sort) {
+            unsigned domain_size = m_dt.get_datatype_num_constructors(s);
+            if (is_unate(s)) {
+                expr_ref one(m_bv.mk_numeral(rational::one(), 1), m);
+                for (unsigned i = 0; i + 2 < domain_size; ++i) {                    
+                    m_imp.m_bounds.push_back(m.mk_implies(m.mk_eq(one, m_bv.mk_extract(i + 1, i + 1, x)),
+                                                          m.mk_eq(one, m_bv.mk_extract(i, i, x))));
+                }
+            }
+            else {
+                if (!is_power_of_two(domain_size) || domain_size == 1) {
+                    m_imp.m_bounds.push_back(m_bv.mk_ule(x, value2bv(domain_size - 1, s)));
+                }             
+            }   
+        }
+
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
             expr_ref a0(m), a1(m);
             expr_ref_vector _args(m);
@@ -65,7 +99,7 @@ struct enum2bv_rewriter::imp {
             }
             else if (m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) {
                 unsigned idx = m_dt.get_recognizer_constructor_idx(f);
-                a1 = m_bv.mk_numeral(rational(idx), get_sort(a0));
+                a1 = value2bv(idx, a0->get_sort());
                 result = m.mk_eq(a0, a1);
                 return BR_DONE;
             }
@@ -92,7 +126,7 @@ struct enum2bv_rewriter::imp {
 
         void check_for_fd(unsigned n, expr* const* args) {
             for (unsigned i = 0; i < n; ++i) {
-                if (m_imp.is_fd(get_sort(args[i]))) {
+                if (m_imp.is_fd(args[i]->get_sort())) {
                     throw_non_fd(args[i]);
                 }
             }
@@ -100,11 +134,12 @@ struct enum2bv_rewriter::imp {
 
         bool reduce_arg(expr* a, expr_ref& result) {
 
-            sort* s = get_sort(a);
+            sort* s = a->get_sort();
             if (!m_imp.is_fd(s)) {
                 return false;
             }
             unsigned bv_size = get_bv_size(s);
+            sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
 
             if (is_var(a)) {
                 result = m.mk_var(to_var(a)->get_idx(), m_bv.mk_sort(bv_size));
@@ -114,7 +149,7 @@ struct enum2bv_rewriter::imp {
             func_decl* f = to_app(a)->get_decl();
             if (m_dt.is_constructor(f)) {
                 unsigned idx = m_dt.get_constructor_idx(f);
-                result = m_bv.mk_numeral(idx, bv_size);
+                result = value2bv(idx, s);
             }
             else if (is_uninterp_const(a)) {
                 func_decl* f_fresh;
@@ -125,17 +160,14 @@ struct enum2bv_rewriter::imp {
 
                 // create a fresh variable, add bounds constraints for it.
                 unsigned nc = m_dt.get_datatype_num_constructors(s);
-                result = m.mk_fresh_const(f->get_name(), m_bv.mk_sort(bv_size));
+                result = m.mk_fresh_const(f->get_name(), bv_sort);
                 f_fresh = to_app(result)->get_decl();
-                if (!is_power_of_two(nc) || nc == 1) {
-                    m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
-                }                
+                constrain_domain(result, s, bv_sort);
                 expr_ref f_def(m);
                 ptr_vector<func_decl> const& cs = *m_dt.get_datatype_constructors(s);
                 f_def = m.mk_const(cs[nc-1]);
-                for (unsigned i = nc - 1; i > 0; ) {
-                    --i;
-                    f_def = m.mk_ite(m.mk_eq(result, m_bv.mk_numeral(i,bv_size)), m.mk_const(cs[i]), f_def);
+                for (unsigned i = nc - 1; i-- > 0; ) {
+                    f_def = m.mk_ite(m.mk_eq(result, value2bv(i, s)), m.mk_const(cs[i]), f_def);
                 }
                 m_imp.m_enum2def.insert(f, f_def);
                 m_imp.m_enum2bv.insert(f, f_fresh);
@@ -169,11 +201,10 @@ struct enum2bv_rewriter::imp {
                 sort* s = q->get_decl_sort(i);
                 if (m_imp.is_fd(s)) {
                     unsigned bv_size = get_bv_size(s);
-                    m_sorts.push_back(m_bv.mk_sort(bv_size));
-                    unsigned nc = m_dt.get_datatype_num_constructors(s);
-                    if (!is_power_of_two(nc) || nc == 1) {
-                        bounds.push_back(m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_bv.mk_numeral(nc-1, bv_size)));
-                    }                
+                    sort* bv_sort = m_bv.mk_sort(bv_size);
+                    m_sorts.push_back(bv_sort);
+                    expr_ref var(m.mk_var(q->get_num_decls()-i-1, bv_sort), m);
+                    constrain_domain(var, s, bv_sort);
                     found = true;
                 }
                 else {
@@ -209,6 +240,8 @@ struct enum2bv_rewriter::imp {
 
         unsigned get_bv_size(sort* s) {
             unsigned nc = m_dt.get_datatype_num_constructors(s);
+            if (is_unate(s))
+                return nc - 1;
             unsigned bv_size = 1;
             while ((unsigned)(1 << bv_size) < nc) {
                 ++bv_size;
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index f1ef304e2..9c963dacd 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -874,7 +874,7 @@ void seq_util::str::get_concat_units(expr* e, expr_ref_vector& es) const {
 }
 
 app* seq_util::str::mk_is_empty(expr* s) const {
-    return m.mk_eq(s, mk_empty(get_sort(s)));
+    return m.mk_eq(s, mk_empty(s->get_sort()));
 }
 
 
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 5a12677b2..76760d705 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -229,11 +229,11 @@ public:
     bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
     bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
     bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT)  && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
-    bool is_seq(expr* e) const  { return is_seq(m.get_sort(e)); }
+    bool is_seq(expr* e) const  { return is_seq(e->get_sort()); }
     bool is_seq(sort* s, sort*& seq) const { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
-    bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
-    bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
-    bool is_char(expr* e) const { return is_char(m.get_sort(e)); }
+    bool is_re(expr* e) const { return is_re(e->get_sort()); }
+    bool is_re(expr* e, sort*& seq) const { return is_re(e->get_sort(), seq); }
+    bool is_char(expr* e) const { return is_char(e->get_sort()); }
     bool is_const_char(expr* e, unsigned& c) const;
     bool is_const_char(expr* e) const { unsigned c; return is_const_char(e, c); }
     bool is_char_le(expr const* e) const;
@@ -344,12 +344,11 @@ public:
         bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_FROM_CODE); }
 
         bool is_string_term(expr const * n) const {
-            sort * s = get_sort(n);
-            return u.is_string(s);
+            return u.is_string(n->get_sort());
         }
 
         bool is_non_string_sequence(expr const * n) const {
-            sort * s = get_sort(n);
+            sort * s = n->get_sort();
             return (u.is_seq(s) && !u.is_string(s));
         }
 
diff --git a/src/muz/spacer/spacer_antiunify.cpp b/src/muz/spacer/spacer_antiunify.cpp
index e5df7c927..867eef884 100644
--- a/src/muz/spacer/spacer_antiunify.cpp
+++ b/src/muz/spacer/spacer_antiunify.cpp
@@ -132,7 +132,7 @@ void anti_unifier::operator()(expr *e1, expr *e2, expr_ref &res,
         unsigned num_arg2 = n2->get_num_args();
         if (n1->get_decl() != n2->get_decl() || num_arg1 != num_arg2) {
             expr_ref v(m);
-            v = m.mk_var(m_subs.size(), get_sort(n1));
+            v = m.mk_var(m_subs.size(), n1->get_sort());
             m_pinned.push_back(v);
             m_subs.push_back(expr_pair(n1, n2));
             m_cache.insert(n1, n2, v);
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 9e348519b..435a3bd14 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -119,7 +119,7 @@ void pob::get_skolems(app_ref_vector &v) {
     for (unsigned i = 0, sz = m_binding.size(); i < sz; ++i) {
         expr* e;
         e = m_binding.get(i);
-        v.push_back (mk_zk_const (get_ast_manager(), i, get_sort(e)));
+        v.push_back (mk_zk_const (get_ast_manager(), i, e->get_sort()));
     }
 }
 
@@ -237,7 +237,7 @@ void derivation::exist_skolemize(expr* fml, app_ref_vector& vars, expr_ref& res)
     expr_safe_replace sub(m);
     for (unsigned i = 0, sz = vars.size(); i < sz; ++i) {
         expr* e = vars.get(i);
-        sub.insert(e, mk_zk_const(m, i, get_sort(e)));
+        sub.insert(e, mk_zk_const(m, i, e->get_sort()));
     }
     sub(fml, res);
 }
@@ -541,7 +541,7 @@ void lemma::mk_expr_core() {
         ptr_buffer<sort> sorts;
         svector<symbol> names;
         for (app* z : zks) {
-            sorts.push_back(get_sort(z));
+            sorts.push_back(z->get_sort());
             names.push_back(z->get_decl()->get_name());
         }
         m_body = m.mk_quantifier(forall_k, zks.size(),
diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index 09e438142..9a63a4a7c 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -195,8 +195,8 @@ public:
     void operator()(app* a)
     {
         if (a->get_family_id() == null_family_id && m_au.is_array(a)) {
-            if (m_sort && m_sort != get_sort(a)) { return; }
-            if (!m_sort) { m_sort = get_sort(a); }
+            if (m_sort && m_sort != a->get_sort()) { return; }
+            if (!m_sort) { m_sort = a->get_sort(); }
             m_symbs.insert(a->get_decl());
         }
     }
diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp
index c0c978b85..141d14719 100644
--- a/src/muz/spacer/spacer_proof_utils.cpp
+++ b/src/muz/spacer/spacer_proof_utils.cpp
@@ -230,7 +230,7 @@ namespace spacer {
             if (a.is_numeral(e)) return false;
             if (!var || var == e) {
                 var = e;
-                val = a.mk_numeral(rational(1), get_sort(e));
+                val = a.mk_numeral(rational(1), e->get_sort());
                 return true;
             }
             return false;
diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp
index 63b204736..e85b7648e 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -226,7 +226,7 @@ expr* times_minus_one(expr *e, arith_util &arith) {
     expr *r;
     if (arith.is_times_minus_one (e, r)) { return r; }
 
-    return arith.mk_mul(arith.mk_numeral(rational(-1), arith.is_int(get_sort(e))), e);
+    return arith.mk_mul(arith.mk_numeral(rational(-1), arith.is_int(e->get_sort())), e);
 }
 }
 
@@ -502,7 +502,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
     expr_ref_vector abs_cube(m);
 
     var_ref var(m);
-    var = m.mk_var (m_offset, get_sort(term));
+    var = m.mk_var (m_offset, term->get_sort());
 
     mk_abs_cube(lemma, term, var, gnd_cube, abs_cube, lb, ub, stride);
     if (abs_cube.empty()) {return false;}
diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp
index c37370d14..15ad66bae 100644
--- a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp
+++ b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp
@@ -65,7 +65,7 @@ namespace datalog {
         for(unsigned i = nb_predicates; i < tail_size; i++) {
             expr* cond = r.get_tail(i);
             expr* e1, *e2;
-            if (m.is_eq(cond, e1, e2) && m_a.is_array(get_sort(e1))) {
+            if (m.is_eq(cond, e1, e2) && m_a.is_array(e1->get_sort())) {
                 array_eq_classes.merge(e1, e2);
             }
             else {
diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp
index 9c962d774..29e4c8c7a 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_array_instantiation.cpp
@@ -103,12 +103,12 @@ namespace datalog {
         expr_ref_vector new_args(m);
         for(unsigned i=0;i<old_head->get_num_args();i++) {
             expr*arg = old_head->get_arg(i);
-            if(m_a.is_array(get_sort(arg))) {
+            if(m_a.is_array(arg->get_sort())) {
                 for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++)  {
                     expr_ref_vector dummy_args(m);
                     dummy_args.push_back(arg);
-                    for(unsigned i=0;i<get_array_arity(get_sort(arg));i++) {
-                        dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(arg), i)));
+                    for(unsigned i=0;i<get_array_arity(arg->get_sort());i++) {
+                        dummy_args.push_back(m.mk_var(cnt, get_array_domain(arg->get_sort(), i)));
                         cnt++;
                     }
                     expr_ref select(m);
@@ -140,7 +140,7 @@ namespace datalog {
         }
         //If it is a select, then add it to selects
         if(m_a.is_select(f)) {
-            SASSERT(!m_a.is_array(get_sort(e)));
+            SASSERT(!m_a.is_array(e->get_sort()));
             selects.insert_if_not_there(f->get_arg(0), ptr_vector<expr>());
             selects[f->get_arg(0)].push_back(e);
         }
@@ -148,7 +148,7 @@ namespace datalog {
         if(m_a.is_store(f)) {
             eq_classes.merge(e, f->get_arg(0));
         }
-        else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0)))) {
+        else if(m.is_eq(f) && m_a.is_array(f->get_arg(0)->get_sort())) {
             eq_classes.merge(f->get_arg(0), f->get_arg(1));
         }
     }
@@ -180,7 +180,7 @@ namespace datalog {
         }
         sort_ref_vector new_sorts(m);
         for(unsigned i=0;i<new_args.size();i++)
-            new_sorts.push_back(get_sort(new_args[i].get()));
+            new_sorts.push_back(new_args.get(i)->get_sort());
         expr_ref res(m);
         func_decl_ref fun_decl(m);
         fun_decl = m.mk_func_decl(symbol((old_pred->get_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range());
@@ -196,7 +196,7 @@ namespace datalog {
         var*result;
         if(!done_selects.find(select, result)) {
             ownership.push_back(select);
-            result = m.mk_var(cnt, get_sort(select));
+            result = m.mk_var(cnt, select->get_sort());
             cnt++;
             done_selects.insert(select, result);
         }
@@ -230,8 +230,8 @@ namespace datalog {
         if(all_selects.empty()) {
             expr_ref_vector dummy_args(m);
             dummy_args.push_back(array);
-            for(unsigned i=0;i<get_array_arity(get_sort(array));i++) {
-                dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(array), i)));
+            for(unsigned i=0;i<get_array_arity(array->get_sort());i++) {
+                dummy_args.push_back(m.mk_var(cnt, get_array_domain(array->get_sort(), i)));
                 cnt++;
             }
             all_selects.push_back(m_a.mk_select(dummy_args.size(), dummy_args.c_ptr()));
@@ -247,7 +247,7 @@ namespace datalog {
         vector<expr_ref_vector> arg_correspondance;
         for(unsigned i=0;i<nb_old_args;i++) {
             expr_ref arg(old_pred->get_arg(i), m);
-            if(m_a.is_array(get_sort(arg))) {
+            if(m_a.is_array(arg->get_sort())) {
                 vector<expr_ref_vector> arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg));
                 arg_correspondance.append(arg_possibilities);
                 if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) {
diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt
index fb61c0c33..d88d11c0f 100644
--- a/src/opt/CMakeLists.txt
+++ b/src/opt/CMakeLists.txt
@@ -5,6 +5,7 @@ z3_add_component(opt
     maxsmt.cpp
     opt_cmds.cpp
     opt_context.cpp
+    opt_lns.cpp
     opt_pareto.cpp
     opt_parse.cpp
     optsmt.cpp
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index cfa2cc61a..722bebc8c 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -62,6 +62,7 @@ Notes:
 #include "smt/smt_solver.h"
 #include "opt/opt_context.h"
 #include "opt/opt_params.hpp"
+#include "opt/opt_lns.h"
 #include "opt/maxsmt.h"
 #include "opt/maxres.h"
 
@@ -107,9 +108,9 @@ private:
                                                // this option is disabled if SAT core is used.
     bool             m_pivot_on_cs;            // prefer smaller correction set to core.
     bool             m_dump_benchmarks;        // display benchmarks (into wcnf format)
-
+    bool             m_enable_lns { false };   // enable LNS improvements
+    unsigned         m_lns_conflicts { 1000 }; // number of conflicts used for LNS improvement
     
-
     std::string      m_trace_id;
     typedef ptr_vector<expr> exprs;
 
@@ -201,6 +202,7 @@ public:
         if (!init()) return l_undef;
         is_sat = init_local();
         trace();
+        improve_model();
         if (is_sat != l_true) return is_sat;
         while (m_lower < m_upper) {
             TRACE("opt_verbose", 
@@ -730,7 +732,29 @@ public:
         add(fml);
     }
 
+    void improve_model() {
+        if (!m_enable_lns)
+            return;
+        model_ref mdl;
+        s().get_model(mdl);
+        if (mdl)
+            update_assignment(mdl);
+    }
+
+    void improve_model(model_ref& mdl) {
+        if (!m_enable_lns) 
+            return;
+        flet<bool> _disable_lns(m_enable_lns, false);
+        std::function<void(model_ref&)> update_model = [&](model_ref& mdl) {
+            update_assignment(mdl);
+        };
+        lns lns(s(), update_model);
+        lns.set_conflicts(m_lns_conflicts);
+        lns.climb(mdl, m_asms);
+    }
+
     void update_assignment(model_ref & mdl) {
+        improve_model(mdl);
         mdl->set_model_completion(true);
         unsigned correction_set_size = 0;
         for (expr* a : m_asms) {
@@ -818,6 +842,8 @@ public:
         m_pivot_on_cs =             p.maxres_pivot_on_correction_set();
         m_wmax =                    p.maxres_wmax();
         m_dump_benchmarks =         p.dump_benchmarks();
+        m_enable_lns =              p.enable_lns() && m_c.sat_enabled();
+        m_lns_conflicts =           p.lns_conflicts();
     }
 
     lbool init_local() {
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 1bdc4d7a5..ad355cc9e 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -73,9 +73,6 @@ namespace opt {
         rational         m_upper;
         model_ref        m_model;
         svector<symbol>  m_labels;
-        //const expr_ref_vector  m_soft;
-        //vector<rational> m_weights;
-        //bool_vector    m_assignment;       // truth assignment to soft constraints
         params_ref       m_params;           // config
 
     public:
diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp
new file mode 100644
index 000000000..a17a71366
--- /dev/null
+++ b/src/opt/opt_lns.cpp
@@ -0,0 +1,168 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    opt_lns.cpp
+
+Abstract:
+   
+    "large" neighborhood search for maxsat problem instances.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-02-01
+
+--*/
+
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_pp.h"
+#include "opt/maxsmt.h"
+#include "opt/opt_lns.h"
+#include "sat/sat_params.hpp"
+#include <algorithm>
+
+namespace opt {
+
+    lns::lns(solver& s, std::function<void(model_ref& mdl)>& update_model)
+        : m(s.get_manager()),
+          s(s),
+          m_hardened(m),
+          m_soft(m),
+          m_update_model(update_model)
+    {}
+
+    void lns::set_lns_params() {
+        params_ref p;
+        p.set_sym("phase", symbol("frozen"));
+        p.set_uint("restart.initial", 1000000);
+        p.set_uint("max_conflicts", m_max_conflicts);    
+        p.set_uint("simplify.delay", 1000000);
+        s.updt_params(p);
+    }
+
+    void lns::save_defaults(params_ref& p) {
+        sat_params sp(p);
+        p.set_sym("phase", sp.phase());
+        p.set_uint("restart.initial", sp.restart_initial());
+        p.set_uint("max_conflicts", sp.max_conflicts());
+        p.set_uint("simplify.delay", sp.simplify_delay());
+    }
+
+    unsigned lns::climb(model_ref& mdl, expr_ref_vector const& asms) {
+        m_num_improves = 0;
+        params_ref old_p(s.get_params());
+        save_defaults(old_p);
+        set_lns_params();
+        setup_assumptions(mdl, asms);
+        unsigned num_improved = improve_linear(mdl);
+//      num_improved += improve_rotate(mdl, asms);
+        s.updt_params(old_p);
+        IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n");
+        return num_improved;
+    }
+
+    void lns::setup_assumptions(model_ref& mdl, expr_ref_vector const& asms) {
+        m_hardened.reset();
+        m_soft.reset();
+        for (expr* a : asms) {
+            if (mdl->is_true(a))
+                m_hardened.push_back(a);
+            else
+                m_soft.push_back(a);
+        }
+    }
+
+    unsigned lns::improve_rotate(model_ref& mdl, expr_ref_vector const& asms) {
+        unsigned num_improved = 0;
+    repeat:
+        setup_assumptions(mdl, asms);
+        unsigned sz = m_hardened.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            expr_ref tmp(m_hardened.get(i), m);
+            m_hardened[i] = m.mk_not(tmp);
+            unsigned reward = improve_linear(mdl);
+            if (reward > 1) {
+                num_improved += (reward - 1);
+                goto repeat;
+            }
+            setup_assumptions(mdl, asms);
+        }
+        return num_improved;
+    }
+
+    unsigned lns::improve_linear(model_ref& mdl) {
+        unsigned num_improved = 0;
+        unsigned max_conflicts = m_max_conflicts;
+        while (m.inc()) {
+            unsigned reward = improve_step(mdl);
+            if (reward == 0)
+                break;
+            num_improved += reward;
+            m_max_conflicts *= 3;
+            m_max_conflicts /= 2;
+            set_lns_params();
+        }
+        m_max_conflicts = max_conflicts;
+        return num_improved;
+    }
+
+    unsigned lns::improve_step(model_ref& mdl) {
+        unsigned num_improved = 0;
+        for (unsigned i = 0; m.inc() && i < m_soft.size(); ++i) {
+            switch (improve_step(mdl, soft(i))) {
+            case l_undef:
+                break;
+            case l_false:
+                TRACE("opt", tout << "pruned " << mk_bounded_pp(soft(i), m) << "\n";);
+                m_hardened.push_back(m.mk_not(soft(i)));
+                for (unsigned k = i; k + 1 < m_soft.size(); ++k) 
+                    m_soft[k] = soft(k + 1);
+                m_soft.pop_back();
+                --i;
+                break;
+            case l_true: {
+                unsigned k = 0, offset = 0;
+                for (unsigned j = 0; j < m_soft.size(); ++j) {
+                    if (mdl->is_true(soft(j))) {
+                        if (j <= i)
+                            ++offset;
+                        ++m_num_improves;                        
+                        TRACE("opt", tout << "improved " << mk_bounded_pp(soft(j), m) << "\n";);
+                        m_hardened.push_back(soft(j));
+                        ++num_improved;
+                    }
+                    else {
+                        m_soft[k++] = soft(j);
+                    }
+                }
+                m_soft.shrink(k);
+                i -= offset;
+                IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n");
+                m_update_model(mdl);
+                break;
+            }       
+            }
+        }
+        return num_improved;
+    }
+
+    lbool lns::improve_step(model_ref& mdl, expr* e) {
+        m_hardened.push_back(e);
+        lbool r = s.check_sat(m_hardened);
+        m_hardened.pop_back();
+        if (r == l_true) 
+            s.get_model(mdl);
+#if 0
+        if (r == l_false) {
+            expr_ref_vector core(m);
+            s.get_unsat_core(core);
+            std::cout << "core size " << core.size() << "\n";
+            if (core.size() == 4)
+                std::cout << core << "\n";
+        }
+#endif
+        return r;
+    } 
+
+};
diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h
new file mode 100644
index 000000000..b84dc14e5
--- /dev/null
+++ b/src/opt/opt_lns.h
@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    opt_lns.h
+
+Abstract:
+   
+    "large" neighborhood search for maxsat problem instances.
+
+    Start with a model that we assume satisfies at least one of the soft constraint assumptions.
+    Attempt to improve the model locally by invoking the SAT solver with a phase
+    fixed to be the assignment that solved the previous instance.
+    Local improvement is performed by hardening each soft constraint in turn.
+    The soft constraints are assumed sorted by weight, such that the highest 
+    weight soft constraint is first, followed by soft constraints of lower weight.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-02-01
+
+--*/
+
+#pragma once
+
+namespace opt {
+
+    class lns {
+        ast_manager&     m;
+        solver&          s;
+        expr_ref_vector  m_hardened;
+        expr_ref_vector  m_soft;
+        unsigned         m_max_conflicts { 1000 };
+        unsigned         m_num_improves { 0 };
+        std::function<void(model_ref& m)> m_update_model;
+
+        expr* soft(unsigned i) const { return m_soft[i]; }
+        void  set_lns_params();
+        void  save_defaults(params_ref& p);
+        unsigned improve_step(model_ref& mdl);
+        lbool improve_step(model_ref& mdl, expr* e);
+        unsigned improve_linear(model_ref& mdl);
+        unsigned improve_rotate(model_ref& mdl, expr_ref_vector const& asms);
+        void  setup_assumptions(model_ref& mdl, expr_ref_vector const& asms);
+
+    public:
+        lns(solver& s, std::function<void(model_ref&)>& update_model);
+        void set_conflicts(unsigned c) { m_max_conflicts = c; }
+        unsigned climb(model_ref& mdl, expr_ref_vector const& asms);
+    };
+};
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index e93a8b973..2192ed9ce 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -9,7 +9,9 @@ def_module_params('opt',
                           ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"),
                           ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
                           ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
-                          ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
+                          ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'),
+                          ('enable_lns', BOOL, False, 'enable LNS during weighted maxsat'),
+                          ('lns_conflicts', UINT, 1000, 'initial conflict count for LNS search'),
                           ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
                           ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp
index 3916da38b..bed96a0b7 100644
--- a/src/qe/mbp/mbp_term_graph.cpp
+++ b/src/qe/mbp/mbp_term_graph.cpp
@@ -42,7 +42,7 @@ namespace mbp {
     namespace {
         struct sort_lt_proc {
             bool operator()(const expr* a, const expr *b) const {
-                return get_sort(a)->get_id() < get_sort(b)->get_id();
+                return a->get_sort()->get_id() < b->get_sort()->get_id();
             }
         };
     }
@@ -266,7 +266,7 @@ namespace mbp {
         expr *a = nullptr, *b = nullptr;
         // deal with equality using sort of range
         if (m.is_eq (lit, a, b)) {
-            return get_sort (a)->get_family_id();
+            return a->get_sort()->get_family_id();
         }
         // extract family_id of top level app
         else if (is_app(lit)) {
@@ -919,9 +919,9 @@ namespace mbp {
             unsigned i = 0;
             unsigned sz = reps.size();
             while (i < sz) {
-                sort* last_sort = get_sort(reps.get(i));
+                sort* last_sort = res.get(i)->get_sort();
                 unsigned j = i + 1;
-                while (j < sz && last_sort == get_sort(reps.get(j))) {++j;}
+                while (j < sz && last_sort == reps.get(j)->get_sort()) {++j;}
                 if (j - i == 2) {
                     expr_ref d(m);
                     d = mk_neq(m, reps.get(i), reps.get(i+1));
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index bc2b5339a..947d298b9 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -291,9 +291,9 @@ namespace qel {
             if (m.is_eq(e, lhs, rhs) && trivial_solve(lhs, rhs, e, vs, ts)) {
                 return true;
             }
-            family_id fid = get_sort(e)->get_family_id();
+            family_id fid = e->get_sort()->get_family_id();
             if (m.is_eq(e, lhs, rhs)) {
-                fid = get_sort(lhs)->get_family_id();
+                fid = lhs->get_sort()->get_family_id();
             }
             auto* p = m_solvers.get_plugin(fid);
             if (p) {
diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
index c08f448bf..a5732d3ac 100644
--- a/src/sat/sat_big.cpp
+++ b/src/sat/sat_big.cpp
@@ -198,7 +198,7 @@ namespace sat {
                         s.m_mc.stackv().reset(); // TBD: brittle code
                         s.add_ate(~u, v);
                         if (find_binary_watch(wlist, ~v)) {
-                            IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
+                            IF_VERBOSE(20, verbose_stream() << "binary: " << ~u << "\n");
                             s.assign_unit(~u);
                         }
                         // could turn non-learned non-binary tautology into learned binary.
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 66d660366..877653bf6 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -60,6 +60,8 @@ namespace sat {
             m_phase = PS_SAT_CACHING;
         else if (s == symbol("random"))
             m_phase = PS_RANDOM;
+        else if (s == symbol("frozen"))
+            m_phase = PS_FROZEN;
         else
             throw sat_param_exception("invalid phase selection strategy: always_false, always_true, basic_caching, caching, random");
 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index ab97bf92a..65ceaeb54 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -28,6 +28,7 @@ namespace sat {
         PS_ALWAYS_FALSE,
         PS_BASIC_CACHING,
         PS_SAT_CACHING,
+        PS_FROZEN,
         PS_RANDOM
     };
 
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 062b6904d..8ede44857 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -222,7 +222,6 @@ namespace sat {
         e.m_clause.append(c.size(), c.begin());
     }
 
-
     void model_converter::insert(entry & e, clause const & c) {
         SASSERT(c.contains(e.var()));
         SASSERT(m_entries.begin() <= &e);
@@ -345,7 +344,7 @@ namespace sat {
     void model_converter::flush(model_converter & src) {
         VERIFY(this != &src);
         m_entries.append(src.m_entries);
-        m_exposed_lim = src.m_exposed_lim;
+        m_exposed_lim += src.m_exposed_lim;
         src.m_entries.reset();
         src.m_exposed_lim = 0;
     }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index ba1309d0c..09588a77b 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1682,6 +1682,9 @@ namespace sat {
             case PS_BASIC_CACHING:
                 phase = m_phase[next];
                 break;
+            case PS_FROZEN:
+                phase = m_best_phase[next];
+                break;
             case PS_SAT_CACHING:
                 if (m_search_state == s_unsat) {
                     phase = m_phase[next];
@@ -2071,6 +2074,7 @@ namespace sat {
             if (!was_eliminated(v)) {
                 m_model[v] = value(v);
                 m_phase[v] = value(v) == l_true;
+                m_best_phase[v] = value(v) == l_true;
             }
         }
         TRACE("sat_mc_bug", m_mc.display(tout););
@@ -2847,6 +2851,8 @@ namespace sat {
     }
 
     void solver::updt_phase_of_vars() {
+        if (m_config.m_phase == PS_FROZEN)
+            return;
         unsigned from_lvl = m_conflict_lvl;
         unsigned head = from_lvl == 0 ? 0 : m_scopes[from_lvl - 1].m_trail_lim;
         unsigned sz   = m_trail.size();
@@ -2912,6 +2918,8 @@ namespace sat {
         case PS_ALWAYS_FALSE:
             for (auto& p : m_phase) p = false;
             break;
+        case PS_FROZEN:
+            break;
         case PS_BASIC_CACHING:
             switch (m_rephase_lim % 4) {
             case 0:
diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp
index 9bed103f4..67ff49c98 100644
--- a/src/sat/smt/ba_solver.cpp
+++ b/src/sat/smt/ba_solver.cpp
@@ -1437,6 +1437,10 @@ namespace sat {
 
 
     bool ba_solver::init_watch(constraint& c) {
+        if (c.is_xr()) {
+            std::cout << c.is_xr() << "\n";
+        }
+
         return !inconsistent() && c.init_watch(*this);
     }
 
@@ -2064,8 +2068,10 @@ namespace sat {
             for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
             for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);    
             unit_strengthen();
-            extract_xor();
-            merge_xor();
+            if (s().get_config().m_xor_solver) {
+                extract_xor();
+                merge_xor();
+            }
             cleanup_clauses();
             cleanup_constraints();
             update_pure();
@@ -2073,6 +2079,8 @@ namespace sat {
         }        
         while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size()));
 
+        gc();
+
         // validate_eliminated();
 
         IF_VERBOSE(1, 
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 47c28de16..bd99336c0 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -72,7 +72,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     expr_ref_vector             m_trail;
     func_decl_ref_vector        m_unhandled_funs;
     bool                        m_default_external;
-    bool                        m_xor_solver;
+    bool                        m_xor_solver { false };
     bool                        m_euf { false };
     bool                        m_drat { false };
     bool                        m_is_redundant { false };
@@ -1020,6 +1020,7 @@ void sat2goal::mc::flush_gmc() {
     expr_ref_vector tail(m);
     expr_ref def(m);
     auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); };
+    
     for (unsigned i = 0; i < updates.size(); ++i) {
         sat::literal l = updates[i];
         if (l == sat::null_literal) {
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 59218f38d..49d3e74ce 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1558,7 +1558,7 @@ namespace smt {
                     // See Section 4.1 in the paper "Complete Quantifier Instantiation"
                     node* S_q_i = slv.get_uvar(q, m_var_i);
                     for (enode* n : ctx->enodes()) {
-                        if (ctx->is_relevant(n) && get_sort(n->get_owner()) == s) {
+                        if (ctx->is_relevant(n) && n->get_owner()->get_sort() == s) {
                             S_q_i->insert(n->get_owner(), n->get_generation());
                         }
                     }
diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index 5ea56fcbb..3b18222af 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -41,7 +41,7 @@ class dt2bv_tactic : public tactic {
     obj_hashtable<sort> m_non_fd_sorts;
     
 
-    bool is_fd(expr* a) { return is_fd(get_sort(a)); }
+    bool is_fd(expr* a) { return is_fd(a->get_sort()); }
     bool is_fd(sort* a) { return m_dt.is_enum_sort(a); }
 
     struct check_fd {        
@@ -59,14 +59,14 @@ class dt2bv_tactic : public tactic {
             }
             else if (m_t.m_dt.is_recognizer(a->get_decl()) &&
                 m_t.is_fd(a->get_arg(0))) {
-                m_t.m_fd_sorts.insert(get_sort(a->get_arg(0)));
+                m_t.m_fd_sorts.insert(a->get_arg(0)->get_sort());
             }
             else if (m_t.is_fd(a) && a->get_num_args() > 0) {
-                m_t.m_non_fd_sorts.insert(get_sort(a));
+                m_t.m_non_fd_sorts.insert(a->get_sort());
                 args_cannot_be_fd(a);
             }
             else if (m_t.is_fd(a)) {
-                m_t.m_fd_sorts.insert(get_sort(a));
+                m_t.m_fd_sorts.insert(a->get_sort());
             }
             else {
                 args_cannot_be_fd(a);
@@ -76,14 +76,14 @@ class dt2bv_tactic : public tactic {
         void args_cannot_be_fd(app* a) {
             for (expr* arg : *a) {
                 if (m_t.is_fd(arg)) {
-                    m_t.m_non_fd_sorts.insert(get_sort(arg));
+                    m_t.m_non_fd_sorts.insert(arg->get_sort());
                 }                    
             }
         }
 
         void operator()(var * v) {
             if (m_t.is_fd(v)) {
-                m_t.m_fd_sorts.insert(get_sort(v));
+                m_t.m_fd_sorts.insert(v->get_sort());
             }
         }
 
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index dbed42ff2..a9b3b71cd 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -242,7 +242,7 @@ private:
 
         if (mc) {
             ensure_mc(mc);
-            expr_ref num(m_bv.mk_numeral(mdl, get_sort(fst_arg)), m);
+            expr_ref num(m_bv.mk_numeral(mdl, fst_arg->get_sort()), m);
             for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) {
                 (*mc)->add(a->get_arg(i), num);
             }
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index 97f05c17b..f2702e245 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -48,7 +48,7 @@ struct is_non_fp_qfnra_predicate {
         if (fid != null_family_id && fid != fu.get_family_id())
             throw found();
 
-        sort * s = get_sort(n);
+        sort * s = n->get_sort();
         if (fid == fu.get_family_id()) {
             if (!fu.is_float(s) && !fu.is_rm(s) &&
                 to_app(n)->get_decl_kind() != OP_FPA_TO_REAL)
@@ -123,7 +123,7 @@ struct is_non_qffp_predicate {
     void operator()(quantifier *) { throw found(); }
 
     void operator()(app * n) {
-        sort * s = get_sort(n);
+        sort * s = n->get_sort();
         if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s))
             throw found();
         family_id fid = n->get_family_id();
diff --git a/src/tactic/fpa/qffplra_tactic.cpp b/src/tactic/fpa/qffplra_tactic.cpp
index 605232772..0fdad5943 100644
--- a/src/tactic/fpa/qffplra_tactic.cpp
+++ b/src/tactic/fpa/qffplra_tactic.cpp
@@ -57,7 +57,7 @@ struct is_non_qffplra_predicate {
     void operator()(quantifier *) { throw found(); }
 
     void operator()(app * n) {
-        sort * s = get_sort(n);
+        sort * s = n->get_sort();
         if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s))
             throw found();
         family_id fid = n->get_family_id();
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 886b2d040..930328085 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -18,6 +18,7 @@ Notes:
 
 --*/
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_util.h"
 #include "ast/occurs.h"
@@ -31,6 +32,7 @@ Notes:
 generic_model_converter::~generic_model_converter() {
 }
 
+
 void generic_model_converter::add(func_decl * d, expr* e) {
     VERIFY(e);
     VERIFY(d->get_range() == m.get_sort(e));