diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 03600131e..b60022f21 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -437,7 +437,7 @@ public:
     void log_bv_from_exprs(app * r, unsigned n, expr* const* es) {
         if (m_manager.has_trace_stream()) {
             for (unsigned i = 0; i < n; ++i) {
-                if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i]))
+                if (!m_manager.is_true(es[i]) && !m_manager.is_false(es[i]))
                     return;
             } 
 
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 2383f62cc..736218bc4 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -254,7 +254,7 @@ namespace smt {
         literal l        = ~(mk_eq(e1->get_owner(), e2->get_owner(), true));
         context & ctx    = get_context();
         ast_manager & m  = get_manager();
-        expr * eq    = ctx.bool_var2expr(l.var());
+        expr * eq        = ctx.bool_var2expr(l.var());
         if (m.has_trace_stream()) {
             app_ref body(m);
             body = m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq));
@@ -1219,7 +1219,7 @@ namespace smt {
 #endif
 
         literal_vector & lits = m_tmp_literals;
-        ptr_vector<expr> exprs;
+        expr_ref_vector exprs(m);
         lits.reset();
         literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true);
         lits.push_back(eq);
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 2ae4dad20..f26791639 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -166,7 +166,7 @@ namespace smt {
         func_decl * d     = n->get_decl();
         ptr_vector<func_decl> const & accessors   = *m_util.get_constructor_accessors(d);
         SASSERT(n->get_num_args() == accessors.size());
-        ptr_vector<app> bindings;
+        app_ref_vector bindings(m);
         vector<std::tuple<enode *, enode *>> used_enodes;
         used_enodes.push_back(std::make_tuple(nullptr, n));
         for (unsigned i = 0; i < n->get_num_args(); ++i) {
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 031988bc6..bc0d0d2e8 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -933,7 +933,7 @@ namespace smt {
             }
         }
         literal_vector lits;
-        ptr_vector<expr> exprs;
+        expr_ref_vector exprs(m);
         for (job_resource const& jr : jrs) {
             unsigned r = jr.m_resource_id;
             res_info const& ri = m_resources[r];
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 49656b05c..e9fbaf81f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1277,7 +1277,7 @@ public:
         if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
             unsigned _k = k.get_unsigned();
             literal_buffer lits;
-            ptr_vector<expr> exprs;
+            expr_ref_vector exprs(m);
             for (unsigned j = 0; j < _k; ++j) {
                 literal mod_j = th.mk_eq(mod, a.mk_int(j), false);
                 lits.push_back(mod_j);
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 46cb3896a..af2d56cf1 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -329,7 +329,7 @@ namespace smt {
         // add case-axioms for all case-paths
         auto & vars = e.m_def->get_vars();
         literal_vector preds;
-        ptr_vector<expr> pred_exprs;
+        expr_ref_vector pred_exprs(m);
         for (recfun::case_def const & c : e.m_def->get_cases()) {
             // applied predicate to `args`
             app_ref pred_applied = c.apply_case_predicate(e.m_args);
@@ -352,7 +352,7 @@ namespace smt {
             }
 
             literal_vector guards;
-            ptr_vector<expr> exprs;
+            expr_ref_vector exprs(m);
             guards.push_back(concl);
             for (auto & g : c.get_guards()) {
                 expr_ref ga = apply_args(depth, vars, e.m_args, g);
@@ -405,7 +405,7 @@ namespace smt {
         expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
 
         literal_vector clause;
-        ptr_vector<expr> exprs;
+        expr_ref_vector exprs(m);
         for (auto & g : e.m_cdef->get_guards()) {
             expr_ref guard = apply_args(depth, vars, args, g);
             clause.push_back(~mk_literal(guard));
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 488d3913e..9a3f47757 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3186,7 +3186,7 @@ bool theory_seq::solve_nc(unsigned idx) {
         TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()) << "\n";);
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
         if (m.has_trace_stream()) {
-            ptr_vector<expr> exprs;
+            expr_ref_vector exprs(m);
             for (literal l : lits) {
                 expr* e = ctx.bool_var2expr(l.var());
                 if (l.sign()) e = m.mk_not(e);
@@ -4642,7 +4642,7 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
     unsigned_vector states;
     a->get_epsilon_closure(a->init(), states);
     lits.push_back(~lit);
-    ptr_vector<expr> exprs;
+    expr_ref_vector exprs(m);
     
     for (unsigned st : states) {
         literal acc = mk_accept(s, zero, re, st);
@@ -5105,7 +5105,7 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
     return lit;
 }
 
-void theory_seq::push_lit_as_expr(literal l, ptr_vector<expr>& buf) {
+void theory_seq::push_lit_as_expr(literal l, expr_ref_vector& buf) {
     expr* e = get_context().bool_var2expr(l.var());
     if (l.sign()) e = m.mk_not(e);
     buf.push_back(e);
@@ -5114,7 +5114,7 @@ void theory_seq::push_lit_as_expr(literal l, ptr_vector<expr>& buf) {
 void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) {
     context& ctx = get_context();
     literal_vector lits;
-    ptr_vector<expr> exprs;
+    expr_ref_vector exprs(m);
     if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return;
     if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); push_lit_as_expr(l1, exprs); }
     if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); push_lit_as_expr(l2, exprs); }
@@ -5672,12 +5672,12 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
     eautomaton::moves mvs;
     aut->get_moves_from(src, mvs);
     TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";);
-    ptr_vector<expr> exprs;
+    expr_ref_vector exprs(m);
     for (auto const& mv : mvs) {
         expr_ref nth = mk_nth(e, idx);
         expr_ref t = mv.t()->accept(nth);
         get_context().get_rewriter()(t);
-        expr* step_e = mk_step(e, idx, re, src, mv.dst(), t);
+        expr_ref step_e(mk_step(e, idx, re, src, mv.dst(), t), m);
         literal step = mk_literal(step_e);
         lits.push_back(step);
         exprs.push_back(step_e);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 5520d4a84..166c8774e 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -547,7 +547,7 @@ namespace smt {
         // terms whose meaning are encoded using axioms.
         void enque_axiom(expr* e);
         void deque_axiom(expr* e);
-        void push_lit_as_expr(literal l, ptr_vector<expr>& buf);
+        void push_lit_as_expr(literal l, expr_ref_vector& buf);
         void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);        
         void add_indexof_axiom(expr* e);
         void add_replace_axiom(expr* e);