From 937b61fc88c209b4ff25123e9c86d640b9ce5acc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 Feb 2021 05:26:57 -0800
Subject: [PATCH] fix build, refactor

---
 src/ackermannization/ackr_model_converter.cpp |  2 +-
 src/ackermannization/lackr.cpp                |  8 +--
 .../lackr_model_constructor.cpp               |  2 +-
 src/ast/fpa/fpa2bv_converter.cpp              |  8 +--
 src/ast/rewriter/enum2bv_rewriter.cpp         |  4 +-
 src/ast/rewriter/expr_safe_replace.cpp        |  2 +-
 src/ast/rewriter/func_decl_replace.cpp        |  2 +-
 src/cmd_context/cmd_context.cpp               |  4 +-
 src/cmd_context/extra_cmds/dbg_cmds.cpp       |  2 +-
 src/opt/opt_lns.cpp                           | 18 +++++--
 src/opt/opt_lns.h                             |  5 ++
 src/parsers/smt2/smt2parser.cpp               | 10 ++--
 src/qe/mbp/mbp_arrays.cpp                     |  4 +-
 src/qe/nlarith_util.cpp                       |  2 +-
 src/qe/qe.cpp                                 |  2 +-
 src/qe/qe_arith_plugin.cpp                    |  2 +-
 src/qe/qe_array_plugin.cpp                    |  6 +--
 src/qe/qe_dl_plugin.cpp                       |  6 +--
 src/qe/qe_lite.cpp                            |  2 +-
 src/qe/qe_mbp.cpp                             |  4 +-
 src/sat/smt/arith_solver.cpp                  |  4 +-
 src/sat/smt/array_axioms.cpp                  |  6 +--
 src/sat/smt/dt_solver.cpp                     |  2 +-
 src/sat/smt/q_mbi.cpp                         |  2 +-
 src/sat/smt/q_solver.cpp                      |  2 +-
 src/smt/arith_eq_adapter.cpp                  |  2 +-
 src/smt/seq_axioms.cpp                        |  4 +-
 src/smt/seq_skolem.cpp                        |  4 +-
 src/smt/seq_skolem.h                          |  2 +-
 src/smt/smt_consequences.cpp                  |  2 +-
 src/smt/smt_context.cpp                       |  2 +-
 src/smt/smt_implied_equalities.cpp            |  8 +--
 src/smt/smt_induction.cpp                     |  8 +--
 src/smt/smt_internalizer.cpp                  |  6 +--
 src/smt/smt_model_finder.cpp                  |  4 +-
 src/smt/smt_model_generator.cpp               |  2 +-
 src/smt/smt_quick_checker.cpp                 |  2 +-
 src/smt/theory_array.cpp                      |  2 +-
 src/smt/theory_array_base.cpp                 |  8 +--
 src/smt/theory_array_base.h                   |  2 +-
 src/smt/theory_array_full.cpp                 |  4 +-
 src/smt/theory_bv.cpp                         |  2 +-
 src/smt/theory_bv.h                           |  2 +-
 src/smt/theory_datatype.cpp                   | 10 ++--
 src/smt/theory_dense_diff_logic_def.h         |  2 +-
 src/smt/theory_fpa.cpp                        |  2 +-
 src/smt/theory_str.cpp                        |  2 +-
 src/smt/theory_utvpi.h                        |  2 +-
 src/tactic/arith/eq2bv_tactic.cpp             |  6 +--
 src/tactic/bv/bv_bounds_tactic.cpp            | 11 ++--
 src/tactic/bv/bvarray2uf_rewriter.cpp         |  4 +-
 src/tactic/core/symmetry_reduce_tactic.cpp    |  2 +-
 src/tactic/fd_solver/smtfd_solver.cpp         | 54 +++++++++----------
 53 files changed, 145 insertions(+), 127 deletions(-)

diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index e845d620b..ba3086395 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/src/ackermannization/ackr_model_converter.cpp
@@ -133,7 +133,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
     app* A = to_app(term->get_arg(0));
     expr * e = nullptr, *c = nullptr;
     if (!array_interpretations.find(A, e)) {
-        e = autil.mk_const_array(m.get_sort(A), value);
+        e = autil.mk_const_array(A->get_sort(), value);
     }
     else {
         // avoid storing the same as the default value.
diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp
index 0b3cda595..3a310cc34 100644
--- a/src/ackermannization/lackr.cpp
+++ b/src/ackermannization/lackr.cpp
@@ -175,12 +175,12 @@ void lackr::abstract_fun(fun2terms_map const& apps) {
     for (auto const& kv : apps) {
         func_decl* fd = kv.m_key;
         for (app * t : kv.m_value->var_args) {
-            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
+            app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);
         }
         for (app * t : kv.m_value->const_args) {
-            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
+            app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);
         }
@@ -192,11 +192,11 @@ void lackr::abstract_sel(sel2terms_map const& apps) {
     for (auto const& kv : apps) {
         func_decl * fd = kv.m_key->get_decl();
         for (app * t : kv.m_value->const_args) {
-            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
+            app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             m_info->set_abstr(t, fc);
         }
         for (app * t : kv.m_value->var_args) {
-            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
+            app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             m_info->set_abstr(t, fc);
         }
     }
diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp
index ac5a5cb3b..73caa579a 100644
--- a/src/ackermannization/lackr_model_constructor.cpp
+++ b/src/ackermannization/lackr_model_constructor.cpp
@@ -325,7 +325,7 @@ private:
             if (k == OP_EQ) {
                 // theory dispatch for =
                 SASSERT(num == 2);
-                family_id s_fid = m.get_sort(values.get(0))->get_family_id();
+                family_id s_fid = values[0]->get_sort()->get_family_id();
                 if (s_fid == m_bv_rw.get_fid())
                     m_bv_rw.mk_eq_core(values.get(0), values.get(1), result);
             } else {
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index d16daa22d..698f825c9 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2415,7 +2415,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
     }
     else if (num == 2 &&
         m_util.is_rm(args[0]) &&
-        m_util.is_float(m.get_sort(args[1]))) {
+        m_util.is_float(args[1]->get_sort())) {
         // rm + float -> float
         mk_to_fp_float(f, f->get_range(), args[0], args[1], result);
     }
@@ -3223,7 +3223,7 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
     else {
         expr_ref nw = nan_wrap(args[0]);
 
-        sort * domain[1] = { m.get_sort(nw) };
+        sort * domain[1] = { nw->get_sort() };
         func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
         result = m.mk_app(f_bv, nw);
 
@@ -3439,7 +3439,7 @@ void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr *
     else {
         expr * rm_bv = to_app(args[0])->get_arg(0);
         expr_ref nw = nan_wrap(args[1]);
-        sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(nw) };
+        sort * domain[2] = { rm_bv->get_sort(), nw->get_sort() };
         func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
         result = m.mk_app(f_bv, rm_bv, nw);
     }
@@ -3456,7 +3456,7 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr
     else {
         expr * n = args[0];
         expr_ref nw = nan_wrap(n);
-        sort * domain[1] = { m.get_sort(nw) };
+        sort * domain[1] = { nw->get_sort() };
         func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
         result = m.mk_app(f_bv, nw);
     }
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index 456ce45eb..ff9868735 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -64,9 +64,9 @@ struct enum2bv_rewriter::imp {
             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);
+                return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort.get());
             else 
-                return m_bv.mk_numeral(rational(idx), bv_sort);
+                return m_bv.mk_numeral(rational(idx), bv_sort.get());
         }
 
         void constrain_domain(expr* x, sort* s, sort* bv_sort) {
diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp
index b3bb06e91..d0273be6e 100644
--- a/src/ast/rewriter/expr_safe_replace.cpp
+++ b/src/ast/rewriter/expr_safe_replace.cpp
@@ -99,7 +99,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
                 if (d) {
                     m_args.push_back(d);
                     arg_differs |= arg != d;
-                    SASSERT(arg->get_sort() == m.get_sort(d));
+                    SASSERT(arg->get_sort() == d->get_sort());
                 }
                 else {
                     m_todo.push_back(arg);
diff --git a/src/ast/rewriter/func_decl_replace.cpp b/src/ast/rewriter/func_decl_replace.cpp
index fa034ff6b..266088f43 100644
--- a/src/ast/rewriter/func_decl_replace.cpp
+++ b/src/ast/rewriter/func_decl_replace.cpp
@@ -43,7 +43,7 @@ expr_ref func_decl_replace::operator()(expr* e) {
                 if (m_cache.find(arg, d)) {
                     m_args.push_back(d);
                     arg_differs |= arg != d;
-                    SASSERT(arg->get_sort() == m.get_sort(d));
+                    SASSERT(arg->get_sort() == d->get_sort());
                 }
                 else {
                     m_todo.push_back(arg);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index ae2eb1c80..f55e3ad1d 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -327,7 +327,7 @@ bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, exp
         bool eq = true;
         coerced_args.reset();
         for (unsigned i = 0; eq && i < n; ++i) {
-            if (d.m_domain[i] == m().get_sort(args[i])) {
+            if (d.m_domain[i] == args[i]->get_sort()) {
                 coerced_args.push_back(args[i]);
                 continue;
             }
@@ -1132,7 +1132,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
             bool first = true;
             for (unsigned i = 0; i < num_args; ++i, first = false) {
                 if (!first) buffer << " ";
-                buffer << mk_pp(m().get_sort(args[i]), m());
+                buffer << mk_pp(args[i]->get_sort(), m());
             }            
             buffer << ") ";
             if (range) buffer << mk_pp(range, m()) << " ";
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index 6f63a5aee..fad351e64 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -293,7 +293,7 @@ public:
             throw cmd_exception("invalid command, mismatch between the number of quantified variables and the number of arguments.");
         unsigned i = num;
         while (i-- > 0) {
-            sort * s = ctx.m().get_sort(ts[i]);
+            sort * s = ts[i]->get_sort();
             if (s != m_q->get_decl_sort(i)) {
                 std::ostringstream buffer;
                 buffer << "invalid command, sort mismatch at position " << i;
diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp
index a17a71366..a9439cf22 100644
--- a/src/opt/opt_lns.cpp
+++ b/src/opt/opt_lns.cpp
@@ -65,6 +65,12 @@ namespace opt {
     void lns::setup_assumptions(model_ref& mdl, expr_ref_vector const& asms) {
         m_hardened.reset();
         m_soft.reset();
+        std::cout << "disjoint cores: " << m_cores.size() << "\n";
+        for (auto const& c : m_cores)
+            std::cout << c.size() << "\n";
+        m_was_flipped.reset();
+        m_in_core.reset();
+        m_cores.reset();
         for (expr* a : asms) {
             if (mdl->is_true(a))
                 m_hardened.push_back(a);
@@ -118,6 +124,7 @@ namespace opt {
                 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_was_flipped.mark(m_hardened.back());
                 m_soft.pop_back();
                 --i;
                 break;
@@ -157,9 +164,14 @@ namespace opt {
         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";
+            bool was_flipped = false;
+            for (expr* c : core) 
+                was_flipped |= m_was_flipped.is_marked(c);
+            if (!was_flipped) {
+                for (expr* c : core) 
+                    m_in_core.mark(c, true);
+                m_cores.push_back(core);
+            }
         }
 #endif
         return r;
diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h
index b84dc14e5..41e33ab81 100644
--- a/src/opt/opt_lns.h
+++ b/src/opt/opt_lns.h
@@ -33,6 +33,11 @@ namespace opt {
         expr_ref_vector  m_soft;
         unsigned         m_max_conflicts { 1000 };
         unsigned         m_num_improves { 0 };
+
+        vector<expr_ref_vector> m_cores;
+        expr_mark               m_in_core;
+        expr_mark               m_was_flipped;
+
         std::function<void(model_ref& m)> m_update_model;
 
         expr* soft(unsigned i) const { return m_soft[i]; }
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index f205c3bd1..825598f7a 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1444,7 +1444,7 @@ namespace smt2 {
         // compute match condition and substitution
         // t is shifted by size of subst.
         expr_ref bind_match(expr* t, expr* pattern, expr_ref_vector& subst) {
-            if (t->get_sort() != m().get_sort(pattern)) {
+            if (t->get_sort() != pattern->get_sort()) {
                 std::ostringstream str;
                 str << "sorts of pattern " << expr_ref(pattern, m()) << " and term " 
                     << expr_ref(t, m()) << " are not aligned";
@@ -2271,7 +2271,7 @@ namespace smt2 {
             unsigned num_vars  = parse_sorted_vars();
             parse_sort("Invalid function definition");
             parse_expr();
-            if (m().get_sort(expr_stack().back()) != sort_stack().back())
+            if (expr_stack().back()->get_sort() != sort_stack().back())
                 throw parser_exception("invalid function/constant definition, sort mismatch");
             sort* const* sorts = sort_stack().c_ptr() + sort_spos;
             expr* t = expr_stack().back();
@@ -2427,11 +2427,11 @@ namespace smt2 {
             symbol_stack().shrink(sym_spos);
             m_env.end_scope();
             m_num_bindings = 0;
-            if (m().get_sort(body) != f->get_range()) {
+            if (body->get_sort() != f->get_range()) {
                 std::ostringstream buffer;
                 buffer << "invalid function definition, sort mismatch. Expcected "
                        << mk_pp(f->get_range(), m()) << " but function body has sort "
-                       << mk_pp(m().get_sort(body), m());
+                       << mk_pp(body->get_sort(), m());
                 throw parser_exception(buffer.str());
             }
             m_ctx.insert_rec_fun(f, bindings, ids, body);
@@ -2448,7 +2448,7 @@ namespace smt2 {
             next();
             parse_sort("Invalid constant definition");
             parse_expr();
-            if (m().get_sort(expr_stack().back()) != sort_stack().back())
+            if (expr_stack().back()->get_sort() != sort_stack().back())
                 throw parser_exception("invalid constant definition, sort mismatch");
             m_ctx.insert(id, 0, nullptr, expr_stack().back());
             check_rparen("invalid constant definition, ')' expected");
diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp
index acf8321c9..7f9c34fc3 100644
--- a/src/qe/mbp/mbp_arrays.cpp
+++ b/src/qe/mbp/mbp_arrays.cpp
@@ -1257,7 +1257,7 @@ namespace mbp {
             if (s == m_var->x()) {
                 expr_ref result(t, m);
                 expr_ref_vector args(m);
-                sort* range = get_array_range(m.get_sort(s));
+                sort* range = get_array_range(s->get_sort());
                 for (unsigned i = 0; i < idxs.size(); ++i) {
                     app_ref var(m), sel(m);
                     expr_ref val(m);
@@ -1559,7 +1559,7 @@ namespace mbp {
                 lits.push_back(m.mk_eq(a1, a2));
             }
             else {
-                sort* s = m.get_sort(store->get_arg(indices.size() + 1));
+                sort* s = store->get_arg(indices.size() + 1)->get_sort();
                 for (app* idx : *m_indices[s]) {
                     indices.push_back(idx);
                     assert_store_select(indices, store, mdl, tg, lits);
diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp
index 4a04ec4bb..24b4e64e9 100644
--- a/src/qe/nlarith_util.cpp
+++ b/src/qe/nlarith_util.cpp
@@ -67,7 +67,7 @@ namespace nlarith {
             ast_manager& m = m_lits.get_manager();
             std::string name = m_x->get_decl()->get_name().str();
             name += suffix;
-            sort* r = m.get_sort(m_x);
+            sort* r = m_x->get_sort();
             v= m.mk_const(symbol(name.c_str()), r);
         }
     };
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 2bd264cb9..4199265f5 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2075,7 +2075,7 @@ namespace qe {
                 for (unsigned i = 0; i < num_vars; ++i) {
                     contains_app contains_x(m, vars[i]);
                     if (contains_x(fml)) {
-                        sorts.push_back(m.get_sort(vars[i]));
+                        sorts.push_back(vars[i]->get_sort());
                         names.push_back(vars[i]->get_decl()->get_name());
                         free_vars.push_back(vars[i]);
                     }
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 52c5647eb..30fc92764 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -1037,7 +1037,7 @@ namespace qe {
             app_ref x(m_ctx.get_var(index-1), m);
             app_ref z(m);
             expr_ref p1(m);
-            sort* s = m.get_sort(p);
+            sort* s = p->get_sort();
             if (is_aux) {
                 // An auxiliary variable was introduced in lieu of 'x'.
                 // it has coefficient 'm' = values[index].
diff --git a/src/qe/qe_array_plugin.cpp b/src/qe/qe_array_plugin.cpp
index 775dd0443..96ddc8e2c 100644
--- a/src/qe/qe_array_plugin.cpp
+++ b/src/qe/qe_array_plugin.cpp
@@ -92,7 +92,7 @@ namespace qe {
                 for (unsigned i = 0; i < sz; ++i) {
                     expr_ref save(m);
                     save = lhs = args[i].get();                    
-                    args[i] = arith.mk_numeral(rational(0), m.get_sort(lhs));
+                    args[i] = arith.mk_numeral(rational(0), lhs->get_sort());
                     rhs = arith.mk_uminus(arith.mk_add(args.size(), args.c_ptr()));
                     if (arith.is_mul(lhs, e1, e2) && 
                         arith.is_numeral(e1, r) &&
@@ -165,7 +165,7 @@ namespace qe {
                 expr_ref store_B_i_t(m);
 
                 unsigned num_args = args[0].size();
-                B = m.mk_fresh_const("B", m.get_sort(A));
+                B = m.mk_fresh_const("B", A->get_sort());
                 ptr_buffer<expr> args2;
                 args2.push_back(B);
                 for (unsigned i = 0; i < num_args; ++i) {
@@ -232,7 +232,7 @@ namespace qe {
                 for (unsigned i = args.size(); i > 0; ) {
                     --i;
                     args2.reset();
-                    w = m.mk_fresh_const("w", m.get_sort(args[i].back()));
+                    w = m.mk_fresh_const("w", args[i].back()->get_sort());
                     args2.push_back(store_T);
                     args2.append(args[i]);
                     
diff --git a/src/qe/qe_dl_plugin.cpp b/src/qe/qe_dl_plugin.cpp
index 6e411511d..2791105d9 100644
--- a/src/qe/qe_dl_plugin.cpp
+++ b/src/qe/qe_dl_plugin.cpp
@@ -116,12 +116,12 @@ namespace qe {
     private:
 
         bool is_small_domain(contains_app& x, eq_atoms& eqs, uint64_t& domain_size) {
-            VERIFY(m_util.try_get_size(m.get_sort(x.x()), domain_size));
+            VERIFY(m_util.try_get_size(x.x()->get_sort(), domain_size));
             return domain_size < eqs.num_eqs() + eqs.num_neqs();
         }
 
         void assign_small_domain(contains_app & x,eq_atoms& eqs, unsigned value) {
-            expr_ref vl(m_util.mk_numeral(value, m.get_sort(x.x())), m);
+            expr_ref vl(m_util.mk_numeral(value, x.x()->get_sort()), m);
             expr_ref eq(m.mk_eq(x.x(), vl), m);
             m_ctx.add_constraint(true, eq);
         }
@@ -145,7 +145,7 @@ namespace qe {
         }
 
         void subst_small_domain(contains_app & x,eq_atoms& eqs, unsigned v,expr_ref & fml) {
-            expr_ref vl(m_util.mk_numeral(v, m.get_sort(x.x())), m);
+            expr_ref vl(m_util.mk_numeral(v, x.x()->get_sort()), m);
             m_replace.apply_substitution(x.x(), vl, fml);
         }
 
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index cd17380ac..3f4b48401 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2307,7 +2307,7 @@ public:
         ptr_vector<sort> sorts;
         svector<symbol> names;
         for (unsigned i = 0; i < vars.size(); ++i) {
-            sorts.push_back(m.get_sort(vars[i].get()));
+            sorts.push_back(vars[i]->get_sort());
             names.push_back(vars[i]->get_decl()->get_name());
         }
         q = m.mk_exists(vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qe_lite);
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index d02112338..42c382542 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -55,7 +55,7 @@ class mbproj::impl {
     }
 
     mbp::project_plugin* get_plugin(app* var) {
-        family_id fid = m.get_sort(var)->get_family_id();
+        family_id fid = var->get_sort()->get_family_id();
         return m_plugins.get(fid, nullptr);
     }
 
@@ -168,7 +168,7 @@ class mbproj::impl {
             expr* e1, * e2;
             if (m_array.is_select(n)) {
                 for (expr* arg : *n) {
-                    if (arg->get_sort() == m.get_sort(m_var) && arg != m_var)
+                    if (arg->get_sort() == m_var->get_sort() && arg != m_var)
                         m_res.push_back(arg);
                 }
             }
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 346e53f13..423f719f2 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -313,7 +313,7 @@ namespace arith {
         expr* e2 = n2->get_expr();
         if (m.is_ite(e1) || m.is_ite(e2))
             return;
-        if (e1->get_sort() != m.get_sort(e2))
+        if (e1->get_sort() != e2->get_sort())
             return;
         reset_evidence();
         for (auto const& ev : e)
@@ -612,7 +612,7 @@ namespace arith {
             SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
             if (a.is_int(o) && !r.is_int()) 
                 r = floor(r);
-            value = a.mk_numeral(r, m.get_sort(o));
+            value = a.mk_numeral(r, o->get_sort());
         }
         else if (a.is_arith_expr(o)) {
             expr_ref_vector args(m);
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 32530355d..e3aea9f25 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -425,7 +425,7 @@ namespace array {
 
     bool solver::has_unitary_domain(app* array_term) {
         SASSERT(a.is_array(array_term));
-        sort* s = m.get_sort(array_term);
+        sort* s = array_term->get_sort();
         unsigned dim = get_array_arity(s);
         for (unsigned i = 0; i < dim; ++i) {
             sort* d = get_array_domain(s, i);
@@ -437,7 +437,7 @@ namespace array {
 
     bool solver::has_large_domain(expr* array_term) {
         SASSERT(a.is_array(array_term));
-        sort* s = m.get_sort(array_term);
+        sort* s = array_term->get_sort();
         unsigned dim = get_array_arity(s);
         rational sz(1);
         for (unsigned i = 0; i < dim; ++i) {
@@ -504,7 +504,7 @@ namespace array {
             for (unsigned j = i; j-- > 0; ) {
                 theory_var v2 = roots[j];
                 expr* e2 = var2expr(v2);
-                if (e1->get_sort() != m.get_sort(e2))
+                if (e1->get_sort() != e2->get_sort())
                     continue;
                 if (have_different_model_values(v1, v2))
                     continue;
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 4caec96a3..78ebf32f0 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -511,7 +511,7 @@ namespace dt {
         };
         for (enode* arg : euf::enode_args(parentc)) {
             add(arg);
-            sort* s = m.get_sort(arg->get_expr());
+            sort* s = arg->get_expr()->get_sort();
             if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s)))
                 for (enode* aarg : get_array_args(arg))
                     add(aarg);
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 87f0deb5b..f674c64fc 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -553,7 +553,7 @@ namespace q {
     }
 
     mbp::project_plugin* mbqi::get_plugin(app* var) {
-        family_id fid = m.get_sort(var)->get_family_id();
+        family_id fid = var->get_sort()->get_family_id();
         return m_plugins.get(fid, nullptr);
     }
 
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index a80e5c4d3..8a52d92b7 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -181,7 +181,7 @@ namespace q {
         if (!m_unit_table.empty())
             return;
         for (euf::enode* n : ctx.get_egraph().nodes()) {
-            if (!n->interpreted() && !m.is_uninterp(m.get_sort(n->get_expr())))
+            if (!n->interpreted() && !m.is_uninterp(n->get_expr()->get_sort()))
                 continue;
             expr* e = n->get_expr();
             sort* s = e->get_sort();
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index 6b704568c..b8051ff3d 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -170,7 +170,7 @@ namespace smt {
             ge = m_util.mk_ge(t1, t2);
         }        
         else {
-            sort * st       = m.get_sort(t1);
+            sort * st       = t1->get_sort();
             app_ref minus_one(m_util.mk_numeral(rational::minus_one(), st), m);
             app_ref zero(m_util.mk_numeral(rational::zero(), st), m);
             app_ref t3(m_util.mk_mul(minus_one, t2), m);
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index cf2eb2902..3030b54b5 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -870,7 +870,7 @@ void seq_axioms::add_suffix_axiom(expr* e) {
     add_axiom(lit, s_gt_t, ~mk_eq(y, s));    
 #else
     sort* char_sort = nullptr;
-    VERIFY(seq.is_seq(m.get_sort(s), char_sort));
+    VERIFY(seq.is_seq(s->get_sort(), char_sort));
     expr_ref x = m_sk.mk("seq.suffix.x", s, t);
     expr_ref y = m_sk.mk("seq.suffix.y", s, t);
     expr_ref z = m_sk.mk("seq.suffix.z", s, t);
@@ -899,7 +899,7 @@ void seq_axioms::add_prefix_axiom(expr* e) {
 
 #else
     sort* char_sort = nullptr;
-    VERIFY(seq.is_seq(m.get_sort(s), char_sort));
+    VERIFY(seq.is_seq(s->get_sort(), char_sort));
     expr_ref x = m_sk.mk("seq.prefix.x", s, t);
     expr_ref y = m_sk.mk("seq.prefix.y", s, t);
     expr_ref z = m_sk.mk("seq.prefix.z", s, t);
diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp
index a9657b2ed..d4f16f783 100644
--- a/src/smt/seq_skolem.cpp
+++ b/src/smt/seq_skolem.cpp
@@ -169,7 +169,7 @@ bool seq_skolem::is_post(expr* e, expr*& s, expr*& start) {
 expr_ref seq_skolem::mk_unit_inv(expr* n) {
     expr* u = nullptr;
     VERIFY(seq.str.is_unit(n, u));
-    sort* s = m.get_sort(u);
+    sort* s = u->get_sort();
     return mk(symbol("seq.unit-inv"), n, s);
 }
 
@@ -180,7 +180,7 @@ expr_ref seq_skolem::mk_last(expr* s) {
         return expr_ref(seq.str.mk_char(str, str.length()-1), m);
     }
     sort* char_sort = nullptr;
-    VERIFY(seq.is_seq(m.get_sort(s), char_sort));
+    VERIFY(seq.is_seq(s->get_sort(), char_sort));
     return mk(m_seq_last, s, char_sort);
 }
 
diff --git a/src/smt/seq_skolem.h b/src/smt/seq_skolem.h
index 94c89930d..4e59d2c15 100644
--- a/src/smt/seq_skolem.h
+++ b/src/smt/seq_skolem.h
@@ -82,7 +82,7 @@ namespace smt {
 
         expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); }
         expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); }
-        expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, m.get_sort(t)); }
+        expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, t->get_sort()); }
         expr_ref mk_last(expr* s);
         expr_ref mk_first(expr* s);
         expr_ref mk_pre(expr* s, expr* i) { return mk(m_pre, s, i); }
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 35fbb6146..8760b1c8f 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -318,7 +318,7 @@ namespace smt {
             }
             else {
                 if (!pushed) pushed = true, push();                
-                expr_ref c(m.mk_fresh_const("a", m.get_sort(a)), m);
+                expr_ref c(m.mk_fresh_const("a", a->get_sort()), m);
                 expr_ref eq(m.mk_eq(c, a), m);
                 assert_expr(eq);
                 assumptions.push_back(c);                
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index df519c158..0c23c4578 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4487,7 +4487,7 @@ namespace smt {
     }
 
     bool context::get_value(enode * n, expr_ref & value) {
-        sort * s      = m.get_sort(n->get_owner());
+        sort * s      = n->get_owner()->get_sort();
         family_id fid = s->get_family_id();
         theory * th   = get_theory(fid);
         if (th == nullptr)
diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp
index 494110c49..8722e6701 100644
--- a/src/smt/smt_implied_equalities.cpp
+++ b/src/smt/smt_implied_equalities.cpp
@@ -57,7 +57,7 @@ namespace {
         
         void partition_terms(unsigned num_terms, expr* const* terms, sort2term_ids& termids) {
             for (unsigned i = 0; i < num_terms; ++i) {
-                sort* s = m.get_sort(terms[i]);
+                sort* s = terms[i]->get_sort();
                 term_ids& vec = termids.insert_if_not_there(s, term_ids());
                 vec.push_back(term_id(expr_ref(terms[i],m), i));
             }
@@ -148,7 +148,7 @@ namespace {
             
             SASSERT(!terms.empty());
 
-            sort* srt = m.get_sort(terms[0].term);
+            sort* srt = terms[0].term->get_sort();
                        
             if (m_array_util.is_array(srt)) {
 
@@ -249,7 +249,7 @@ namespace {
 
         void assert_relevant(unsigned num_terms, expr* const* terms) {
             for (unsigned i = 0; i < num_terms; ++i) {                
-                sort* srt = m.get_sort(terms[i]);
+                sort* srt = terms[i]->get_sort();
                 if (!m_array_util.is_array(srt)) {
                     m_solver.assert_expr(m.mk_app(m.mk_func_decl(symbol("Relevant!"), 1, &srt, m.mk_bool_sort()), terms[i]));
                 }
@@ -259,7 +259,7 @@ namespace {
         void assert_relevant(term_ids& terms) {
             for (unsigned i = 0; i < terms.size(); ++i) {
                 expr* t = terms[i].term;
-                sort* srt = m.get_sort(t);
+                sort* srt = t->get_sort();
                 if (!m_array_util.is_array(srt)) {
                     m_solver.assert_expr(m.mk_app(m.mk_func_decl(symbol("Relevant!"), 1, &srt, m.mk_bool_sort()), t));
                 }
diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp
index 4cd8ada8f..6f13a78b9 100644
--- a/src/smt/smt_induction.cpp
+++ b/src/smt/smt_induction.cpp
@@ -136,7 +136,7 @@ bool induction_lemmas::viable_induction_children(enode* n) {
 
 bool induction_lemmas::viable_induction_term(enode* p, enode* n) {
     return 
-        viable_induction_sort(m.get_sort(n->get_owner())) &&
+        viable_induction_sort(n->get_owner()->get_sort()) &&
         viable_induction_parent(p, n) &&
         viable_induction_children(n);
 }
@@ -281,7 +281,7 @@ void induction_lemmas::mk_hypothesis_substs(unsigned depth, expr* x, cond_substs
 }
 
 void induction_lemmas::mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y, expr_ref_vector& conds, cond_substs_t& subst) {
-    sort* ys = m.get_sort(y);
+    sort* ys = y->get_sort();
     for (func_decl* c : *m_dt.get_datatype_constructors(ys)) {
         func_decl* is_c = m_dt.get_constructor_recognizer(c);
         conds.push_back(m.mk_app(is_c, y));
@@ -417,7 +417,7 @@ bool induction_lemmas::operator()(literal lit) {
     for (enode* n : induction_positions(r)) {
         expr* t = n->get_owner();
         if (is_uninterp_const(t)) { // for now, to avoid overlapping terms
-            sort* s = m.get_sort(t);
+            sort* s = t->get_sort();
             expr_ref sk(m.mk_fresh_const("sk", s), m);
             sks.push_back(sk);
             rep.insert(t, sk);
@@ -460,7 +460,7 @@ void induction_lemmas::apply_induction(literal lit, induction_positions_t const
         if (term2skolem.contains(t))
             continue;
         if (i == sks.size()) {
-            sk = m.mk_fresh_const("sk", m.get_sort(t));
+            sk = m.mk_fresh_const("sk", t->get_sort());
             sks.push_back(sk);
         }
         else {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 24f85ca1b..0e1aeef78 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -315,7 +315,7 @@ namespace smt {
             assert_default(n, pr);
             return;
         }
-        sort * s = m.get_sort(n->get_arg(0));
+        sort * s = n->get_arg(0)->get_sort();
         sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
         func_decl_ref f(m.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m);
         for (expr * arg : *n) {
@@ -448,7 +448,7 @@ namespace smt {
         d.set_eq_flag();
         TRACE("internalize", tout << mk_pp(n, m) << " " << literal(v, false) << "\n";);
         
-        sort * s    = m.get_sort(n->get_arg(0));
+        sort * s    = n->get_arg(0)->get_sort();
         theory * th = m_theories.get_plugin(s->get_family_id());
         if (th)
             th->internalize_eq_eh(n, v);
@@ -582,7 +582,7 @@ namespace smt {
         if (e_internalized(q)) {
             return;
         }
-        app_ref lam_name(m.mk_fresh_const("lambda", m.get_sort(q)), m);
+        app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m);
         app_ref eq(m), lam_app(m);
         expr_ref_vector vars(m);
         vars.push_back(lam_name);
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 49d3e74ce..b67187c89 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -654,7 +654,7 @@ namespace smt {
                Remark: this method uses get_fresh_value, so it may fail.
             */
             expr* get_k_interp(app* k) {
-                sort* s = m.get_sort(k);
+                sort* s = k->get_sort();
                 SASSERT(is_infinite(s));
                 func_decl* k_decl = k->get_decl();
                 expr* r = m_model->get_const_interp(k_decl);
@@ -1914,7 +1914,7 @@ namespace smt {
                         if (is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, tmp, inv)) {
                             if (inv)
                                 le = !le;
-                            sort* s = m.get_sort(tmp);
+                            sort* s = tmp->get_sort();
                             expr_ref one(m);
                             one = mk_one(s);
                             if (le)
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index eb0f68b99..382f6d64f 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -307,7 +307,7 @@ namespace smt {
                       enode * n = curr.get_enode();
                       SASSERT(n->get_root() == n);
                       tout << mk_pp(n->get_owner(), m) << "\n";
-                      sort * s = m.get_sort(n->get_owner());
+                      sort * s = n->get_owner()->get_sort();
                       tout << curr << " " << mk_pp(s, m);
                       tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
                   }
diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp
index 14719c140..5dcd1f265 100644
--- a/src/smt/smt_quick_checker.cpp
+++ b/src/smt/smt_quick_checker.cpp
@@ -186,7 +186,7 @@ namespace smt {
             m_candidate_vectors[i].reset();
             sort * s = q->get_decl_sort(i);
             for (unsigned j = 0; j < num_candidates; j++) {
-                if (m_manager.get_sort(candidates[j]) == s) {
+                if (candidates[j]->get_sort() == s) {
                     expr * n = candidates[j];
                     m_context.internalize(n, false);
                     enode * e = m_context.get_enode(n);
diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index 92ca67aeb..e0702f530 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -72,7 +72,7 @@ namespace smt {
               ", is_store: " << is_store(n) << "\n";);
         d->m_is_array  = is_array_sort(n);
         if (d->m_is_array) 
-            register_sort(m.get_sort(n->get_owner()));
+            register_sort(n->get_owner()->get_sort());
         d->m_is_select = is_select(n);        
         if (is_store(n))
             d->m_stores.push_back(n);
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 10038a009..e65c383b6 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -59,7 +59,7 @@ namespace smt {
     }
 
     app * theory_array_base::mk_default(expr * a) {
-        sort * s = m.get_sort(a);
+        sort * s = a->get_sort();
         unsigned num_params = get_dimension(s);
         parameter const* params = s->get_info()->get_parameters();
         return m.mk_app(get_family_id(), OP_ARRAY_DEFAULT, num_params, params, 1, & a);
@@ -564,13 +564,13 @@ namespace smt {
             TRACE("array_bug", tout << "mk_interface_eqs: processing: v" << *it1 << "\n";);
             theory_var  v1 = *it1;
             enode *     n1 = get_enode(v1);
-            sort *      s1 = m.get_sort(n1->get_owner());
+            sort *      s1 = n1->get_owner()->get_sort();
             sbuffer<theory_var>::iterator it2 = it1;
             ++it2;
             for (; it2 != end1; ++it2) {
                 theory_var v2 = *it2;
                 enode *    n2 = get_enode(v2);
-                sort *     s2 = m.get_sort(n2->get_owner());
+                sort *     s2 = n2->get_owner()->get_sort();
                 if (s1 == s2 && !ctx.is_diseq(n1, n2)) {
                     app * eq  = mk_eq_atom(n1->get_owner(), n2->get_owner());
                     if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) {
@@ -983,7 +983,7 @@ namespace smt {
         SASSERT(ctx.is_relevant(n));
         theory_var v       = n->get_th_var(get_id());
         SASSERT(v != null_theory_var);
-        sort * s           = m.get_sort(n->get_owner());
+        sort * s           = n->get_owner()->get_sort();
         enode * else_val_n = get_default(v);
         array_value_proc * result = nullptr;
 
diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h
index 6af1d1f4d..4763c2d9e 100644
--- a/src/smt/theory_array_base.h
+++ b/src/smt/theory_array_base.h
@@ -46,7 +46,7 @@ namespace smt {
         bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); }
         bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
         bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
-        bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); }
+        bool is_array_sort(app const* n) const { return is_array_sort(n->get_sort()); }
         bool is_set_has_size(app const* n) const { return n->is_app_of(get_id(), OP_SET_HAS_SIZE); }
         bool is_set_card(app const* n) const { return n->is_app_of(get_id(), OP_SET_CARD); }
 
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 47f67e9da..782d8e6f6 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -579,7 +579,7 @@ namespace smt {
 
     bool theory_array_full::has_unitary_domain(app* array_term) {
         SASSERT(is_array_sort(array_term));
-        sort* s = m.get_sort(array_term);
+        sort* s = array_term->get_sort();
         unsigned dim = get_dimension(s);
         parameter const * params = s->get_info()->get_parameters();
         for (unsigned i = 0; i < dim; ++i) {
@@ -593,7 +593,7 @@ namespace smt {
 
    bool theory_array_full::has_large_domain(app* array_term) {
         SASSERT(is_array_sort(array_term));
-        sort* s = m.get_sort(array_term);
+        sort* s = array_term->get_sort();
         unsigned dim = get_dimension(s);
         parameter const *  params = s->get_info()->get_parameters();
         rational sz(1);
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 752e899aa..d99bd441d 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -478,7 +478,7 @@ namespace smt {
         VERIFY(get_fixed_value(v, val));
         enode* n = get_enode(v);
         if (ctx.watches_fixed(n)) {
-            expr_ref num(m_util.mk_numeral(val, m.get_sort(n->get_owner())), m);
+            expr_ref num(m_util.mk_numeral(val, n->get_owner()->get_sort()), m);
             literal_vector& lits = m_tmp_literals;
             lits.reset();
             for (literal b : m_bits[v]) {
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 76c78c930..1b1f16603 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -147,7 +147,7 @@ namespace smt {
         unsigned get_bv_size(app const * n) const { return m_util.get_bv_size(n); }
         unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_owner()); }
         unsigned get_bv_size(theory_var v) const { return get_bv_size(get_enode(v)); }
-        bool is_bv(app const* n) const { return m_util.is_bv_sort(get_manager().get_sort(n)); }
+        bool is_bv(app const* n) const { return m_util.is_bv_sort(n->get_sort()); }
         bool is_bv(enode const* n) const { return is_bv(n->get_owner()); }
         bool is_bv(theory_var v) const { return is_bv(get_enode(v)); }
         region & get_region() { return m_trail_stack.get_region(); }
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 02296bcec..1c8907287 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -274,7 +274,7 @@ namespace smt {
             assert_update_field_axioms(n);
         }
         else {
-            sort * s      = m.get_sort(n->get_owner());
+            sort * s      = n->get_owner()->get_sort();
             if (m_util.get_datatype_num_constructors(s) == 1) {
                 func_decl * c = m_util.get_datatype_constructors(s)->get(0);
                 assert_is_constructor_axiom(n, c, null_literal);
@@ -333,7 +333,7 @@ namespace smt {
             //
             for (unsigned i = 0; i < num_args; i++) {
                 enode * arg = e->get_arg(i);
-                sort * s    = m.get_sort(arg->get_owner());
+                sort * s    = arg->get_owner()->get_sort();
                 if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
                     app_ref def(m_autil.mk_default(arg->get_owner()), m);
                     if (!ctx.e_internalized(def)) {
@@ -528,7 +528,7 @@ namespace smt {
                 }
                 found = true;
             }
-            sort * s = m.get_sort(arg->get_owner());
+            sort * s = arg->get_owner()->get_sort();
             if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
                 for (enode* aarg : get_array_args(arg)) {
                     if (aarg->get_root() == child->get_root()) {
@@ -864,7 +864,7 @@ namespace smt {
         unsigned num_unassigned  = 0;
         unsigned unassigned_idx  = UINT_MAX;
         enode * n       = get_enode(v);
-        sort * dt       = m.get_sort(n->get_owner());
+        sort * dt       = n->get_owner()->get_sort();
         var_data * d    = m_var_data[v];
         if (d->m_recognizers.empty()) {
             theory_var w = recognizer->get_arg(0)->get_th_var(get_id());
@@ -947,7 +947,7 @@ namespace smt {
     void theory_datatype::mk_split(theory_var v) {
         v                     = m_find.find(v);
         enode * n             = get_enode(v);
-        sort * s              = m.get_sort(n->get_owner());
+        sort * s              = n->get_owner()->get_sort();
         func_decl * non_rec_c = m_util.get_non_rec_constructor(s); 
         unsigned non_rec_idx  = m_util.get_constructor_idx(non_rec_c);
         var_data * d          = m_var_data[v];
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index e8af0aa75..deab6171e 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -804,7 +804,7 @@ namespace smt {
             enode * n = get_enode(v);
             if (m_autil.is_zero(n->get_owner()) && !m_assignment[v].is_zero()) {
                 numeral val = m_assignment[v];
-                sort * s = m.get_sort(n->get_owner());
+                sort * s = n->get_owner()->get_sort();
                 // adjust the value of all variables that have the same sort.
                 for (int v2 = 0; v2 < num_vars; ++v2) {
                     enode * n2 = get_enode(v2);
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 802fb230d..701161a5f 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -533,7 +533,7 @@ namespace smt {
 
     model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
         TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), m) <<
-                            " (sort " << mk_ismt2_pp(m.get_sort(n->get_owner()), m) << ")\n";);
+                            " (sort " << mk_ismt2_pp(n->get_owner()->get_sort(), m) << ")\n";);
 
         app_ref owner(m);
         owner = get_ite_value(n->get_owner());
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 28161aea4..19c7abb83 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -319,7 +319,7 @@ namespace smt {
     theory_var theory_str::mk_var(enode* n) {
         TRACE("str", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;);
         ast_manager & m = get_manager();
-        if (!(m.get_sort(n->get_owner()) == u.str.mk_string_sort())) {
+        if (!(n->get_owner()->get_sort() == u.str.mk_string_sort())) {
             return null_theory_var;
         }
         if (is_attached_to_var(n)) {
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 6ea13a2f6..1985ed23a 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -328,7 +328,7 @@ namespace smt {
 
         th_var get_zero(sort* s) { return a.is_int(s) ? m_izero : m_rzero; }
 
-        th_var get_zero(expr* e) { return get_zero(get_manager().get_sort(e)); }
+        th_var get_zero(expr* e) { return get_zero(e->get_sort()); }
 
         void init_zero();
 
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 0bd9ffc13..865c268a1 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -35,7 +35,7 @@ class eq2bv_tactic : public tactic {
             expr* z;
             rational r;
             if (t.m_fd.find(x, z) && t.a.is_numeral(y, r)) {
-                result = m.mk_eq(z, t.bv.mk_numeral(r, m.get_sort(z)));
+                result = m.mk_eq(z, t.bv.mk_numeral(r, z->get_sort()));
                 return true;
             }
             else {
@@ -249,13 +249,13 @@ public:
             if (m_bounds.has_lower(c, r, strict) && !r.is_neg()) {
                 SASSERT(!strict);
                 expr* d = m_fd.find(c);
-                fml = bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d);
+                fml = bv.mk_ule(bv.mk_numeral(r, d->get_sort()), d);
                 g->assert_expr(fml, m_bounds.lower_dep(c));
             }
             if (m_bounds.has_upper(c, r, strict) && !r.is_neg()) {
                 SASSERT(!strict);
                 expr* d = m_fd.find(c);
-                fml = bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d)));
+                fml = bv.mk_ule(d, bv.mk_numeral(r, d->get_sort()));
                 g->assert_expr(fml, m_bounds.upper_dep(c));
             }
         }        
diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index 5a9819b69..f4c06b818 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -331,11 +331,12 @@ namespace {
             } else if (m_bound.find(t1, ctx)) {
                 if (ctx.implies(b)) {
                     result = m.mk_true();
-                } else if (!b.intersect(ctx, intr)) {
+                } 
+                else if (!b.intersect(ctx, intr)) {
                     result = m.mk_false();
-                } else if (m_propagate_eq && intr.is_singleton()) {
-                    result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
-                                                         m.get_sort(t1)));
+                } 
+                else if (m_propagate_eq && intr.is_singleton()) {
+                    result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), t1->get_sort()));
                 }
             }
 
@@ -630,7 +631,7 @@ namespace {
                 } 
                 else if (m_propagate_eq && intr.is_singleton()) {
                     r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
-                                                    m.get_sort(t1)));
+                                                    t1->get_sort()));
                 }
                 else {
                     was_updated = false;
diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp
index 014edc3e7..05e895a4c 100644
--- a/src/tactic/bv/bvarray2uf_rewriter.cpp
+++ b/src/tactic/bv/bvarray2uf_rewriter.cpp
@@ -144,7 +144,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
             func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
             func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
 
-            sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
+            sort * sorts[1] = { get_index_sort(args[0]->get_sort()) };
             symbol names[1] = { symbol("x") };
             var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
 
@@ -167,7 +167,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         TRACE("bvarray2uf_rw", tout << "(ite " << c << ", " << f_t->get_name()
             << ", " << f_f->get_name() << ")" << std::endl;);
 
-        sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[1])) };
+        sort * sorts[1] = { get_index_sort(args[1]->get_sort()) };
         symbol names[1] = { symbol("x") };
         var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
 
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 3dbdfde91..aa19428d6 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -258,7 +258,7 @@ private:
           m_manager(m), m_app2sortid(app2sort), m_max_id(0) {}
 
         void operator()(app* n) {
-            sort* s = m_manager.get_sort(n);
+            sort* s = n->get_sort();
             unsigned id;
             if (!m_sort2id.find(s, id)) {
                 id = m_max_id++;
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index d6a92b77d..3f59e1107 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -178,7 +178,7 @@ namespace smtfd {
                 return m.mk_fresh_const(name, m.mk_bool_sort());
             }        
             else if (m_butil.is_bv(t)) {
-                return m.mk_fresh_const(name, m.get_sort(t));
+                return m.mk_fresh_const(name, t->get_sort());
             }
             else {
                 ++m_nv;
@@ -690,7 +690,7 @@ namespace smtfd {
         for (unsigned i = 0; i < a.m_t->get_num_args(); ++i) {
             if (p.values().get(a.m_val_offset+i) != p.values().get(b.m_val_offset+i)) 
                 return false;
-            if (p.get_manager().get_sort(a.m_t->get_arg(i)) != p.get_manager().get_sort(b.m_t->get_arg(i)))
+            if (a.m_t->get_arg(i)->get_sort() != b.m_t->get_arg(i)->get_sort())
                 return false;
         }
         return true;
@@ -793,7 +793,7 @@ namespace smtfd {
         {}
         
         void check_term(expr* t, unsigned round) override {
-            sort* s = m.get_sort(t);
+            sort* s = t->get_sort();
             if (round == 0 && is_uf(t)) {
                 TRACE("smtfd_verbose", tout << "check-term: " << mk_bounded_pp(t, m, 2) << "\n";);
                 enforce_congruence(to_app(t)->get_decl(), to_app(t), s);
@@ -816,7 +816,7 @@ namespace smtfd {
         }
 
         bool term_covered(expr* t) override {
-            sort* s = m.get_sort(t);
+            sort* s = t->get_sort();
             if (sort_covered(s)) {
                 val2elem_t& v2e = get_table(s);
                 expr_ref v = eval_abs(t);
@@ -864,7 +864,7 @@ namespace smtfd {
                 mdl->register_decl(fn, fi);
             }
             for (expr* t : subterms(terms)) {
-                if (is_uninterp_const(t) && sort_covered(m.get_sort(t))) {
+                if (is_uninterp_const(t) && sort_covered(t->get_sort())) {
                     expr_ref val = model_value(t);
                     mdl->register_decl(to_app(t)->get_decl(), val);
                 }
@@ -872,7 +872,7 @@ namespace smtfd {
         }
 
         expr_ref model_value_core(expr* t) override { 
-            sort* s = m.get_sort(t);
+            sort* s = t->get_sort();
             if (sort_covered(s)) {
                 auto& v2e = ensure_table(s);
                 return expr_ref(v2e[eval_abs(t)], m);
@@ -922,14 +922,14 @@ namespace smtfd {
         void insert_select(app* t) {
             expr* a = t->get_arg(0);
             expr_ref vA = eval_abs(a);
-            check_congruence(vA, t, m.get_sort(a));
+            check_congruence(vA, t, a->get_sort());
         }
 
         void check_select(app* t) {
             expr* a = t->get_arg(0);
             expr_ref vA = eval_abs(a);
             TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << "\n";);
-            enforce_congruence(vA, t, m.get_sort(a));                                 
+            enforce_congruence(vA, t, a->get_sort());                                 
         }
 
         // check that (select(t, t.args) = t.value)
@@ -1018,7 +1018,7 @@ namespace smtfd {
             expr_ref vT = eval_abs(t);
             expr_ref vA = eval_abs(arg);
 
-            table& tT = ast2table(vT, m.get_sort(t)); // select table of t
+            table& tT = ast2table(vT, t->get_sort()); // select table of t
             table& tA = ast2table(vA, arg->get_sort()); // select table of arg
 
             if (vT == vA) {                
@@ -1049,7 +1049,7 @@ namespace smtfd {
                 if (m_context.at_max()) {
                     break;
                 }
-                if (m.get_sort(t) != m.get_sort(fA.m_t->get_arg(0))) {
+                if (t->get_sort() != fA.m_t->get_arg(0)->get_sort()) {
                     continue;
                 }
                 if (!tT.find(fA, fT) || (value_of(fA) != value_of(fT) && !eq(m_vargs, fA))) {
@@ -1064,7 +1064,7 @@ namespace smtfd {
                 if (m_context.at_max()) {
                     break;
                 }
-                if (!tA.find(fT, fA) && m.get_sort(t) == m.get_sort(fT.m_t->get_arg(0))) {
+                if (!tA.find(fT, fA) && t->get_sort() == m.get_sort(fT.m_t->get_arg(0))) {
                     TRACE("smtfd", tout << "not found\n";);
                     add_select_store_axiom(t, fT);
                     ++r;
@@ -1080,7 +1080,7 @@ namespace smtfd {
             for (expr* arg : *f.m_t) {
                 m_args.push_back(arg);
             }
-            SASSERT(m.get_sort(t) == m.get_sort(a));
+            SASSERT(t->get_sort() == a->get_sort());
             TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << " " << mk_bounded_pp(f.m_t, m, 2) << "\n";);
             expr_ref eq = mk_eq_idxs(t, f.m_t);
             m_args[0] = t;
@@ -1094,7 +1094,7 @@ namespace smtfd {
         }
 
         bool same_array_sort(f_app const& fA, f_app const& fT) const {
-            return m.get_sort(fA.m_t->get_arg(0)) == m.get_sort(fT.m_t->get_arg(0));
+            return fA.m_t->get_arg(0)->get_sort() == fT.m_t->get_arg(0)->get_sort();
         }
 
         /**
@@ -1105,9 +1105,9 @@ namespace smtfd {
                 m_autil.is_const(t) ||
                 is_lambda(t)) {
                 expr_ref vT = eval_abs(t);
-                table& tT = ast2table(vT, m.get_sort(t));
+                table& tT = ast2table(vT, t->get_sort());
                 for (f_app & f : tT) {
-                    if (m.get_sort(t) != m.get_sort(f.m_t->get_arg(0))) 
+                    if (t->get_sort() != f.m_t->get_arg(0)->get_sort())
                         continue;
                     if (m_context.at_max()) 
                         break;
@@ -1165,7 +1165,7 @@ namespace smtfd {
         }
 
         void enforce_extensionality(expr* a, expr* b) {
-            sort* s = m.get_sort(a);
+            sort* s = a->get_sort();
             unsigned arity = get_array_arity(s);
             expr_ref_vector args(m);
             args.push_back(a);
@@ -1190,7 +1190,7 @@ namespace smtfd {
                 SASSERT(m_autil.is_select(f.m_t));
                 expr_ref v = model_value(f.m_t);
                 if (!value) {
-                    sort* s = m.get_sort(f.m_t->get_arg(0));
+                    sort* s = f.m_t->get_arg(0)->get_sort();
                     default_value = v;
                     value = m_autil.mk_const_array(s, default_value);
                 }
@@ -1256,7 +1256,7 @@ namespace smtfd {
             if (m_autil.is_select(t)) {
                 expr* a = to_app(t)->get_arg(0);
                 expr_ref vA = eval_abs(a);
-                insert(mk_app(vA, to_app(t), m.get_sort(a)));                
+                insert(mk_app(vA, to_app(t), a->get_sort()));                
                 
             }
             return 
@@ -1285,9 +1285,9 @@ namespace smtfd {
         expr_ref model_value_core(expr* t) override { 
             if (m_autil.is_array(t)) {
                 expr_ref vT = eval_abs(t);
-                table& tb = ast2table(vT, m.get_sort(t));
+                table& tb = ast2table(vT, t->get_sort());
                 if (tb.empty()) {
-                    return model_value_core(m.get_sort(t));
+                    return model_value_core(t->get_sort());
                 }
                 else {
                     return mk_array_value(tb);
@@ -1345,7 +1345,7 @@ namespace smtfd {
                 for (unsigned j = i + 1; !m_context.at_max() && j < shared.size(); ++j) {
                     expr* s2 = shared.get(j);
                     expr* v2 = sharedvals.get(j);
-                    if (v1 != v2 && m.get_sort(s1) == m.get_sort(s2) && same_table(v1, m.get_sort(s1), v2, m.get_sort(s2))) {
+                    if (v1 != v2 && s1->get_sort() == s2->get_sort() && same_table(v1, s1->get_sort(), v2, s2->get_sort())) {
                         enforce_extensionality(s1, s2);
                     }
                 }
@@ -1533,8 +1533,8 @@ namespace smtfd {
         void init_term(expr* t) {
             if (!m.is_bool(t) && is_ground(t)) {
                 expr_ref v = eval_abs(t);
-                if (!m_val2term.contains(v, m.get_sort(t))) {
-                    m_val2term.insert(v, m.get_sort(t), t);
+                if (!m_val2term.contains(v, t->get_sort())) {
+                    m_val2term.insert(v, t->get_sort(), t);
                     m_val2term_trail.push_back(v);
                 }
             }
@@ -1725,7 +1725,7 @@ namespace smtfd {
                 }
             }
             for (expr* t : subterms(terms)) {
-                if (!is_forall(t) && !is_exists(t) && (!m_context.term_covered(t) || !m_context.sort_covered(m.get_sort(t)))) {
+                if (!is_forall(t) && !is_exists(t) && (!m_context.term_covered(t) || !m_context.sort_covered(t->get_sort()))) {
                     is_decided = l_false;
                 }
             }
@@ -1739,9 +1739,9 @@ namespace smtfd {
                       if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
                           tout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
                       }
-                      if (!is_forall(a) && !is_exists(a) && (!m_context.term_covered(a) || !m_context.sort_covered(m.get_sort(a)))) {
-                          tout << "not covered: " << mk_pp(a, m) << " " << mk_pp(m.get_sort(a), m) << " "; 
-                          tout << m_context.term_covered(a) << " " << m_context.sort_covered(m.get_sort(a)) << "\n";
+                      if (!is_forall(a) && !is_exists(a) && (!m_context.term_covered(a) || !m_context.sort_covered(a->get_sort()))) {
+                          tout << "not covered: " << mk_pp(a, m) << " " << mk_pp(a->get_sort(), m) << " "; 
+                          tout << m_context.term_covered(a) << " " << m_context.sort_covered(a->get_sort()) << "\n";
                       }
                   }
                   tout << "has quantifier: " << has_q << "\n" << core << "\n";