diff --git a/src/ast/ast_trail.h b/src/ast/ast_trail.h
index 0de2c2c1e..5a76dd537 100644
--- a/src/ast/ast_trail.h
+++ b/src/ast/ast_trail.h
@@ -56,8 +56,8 @@ public:
     }
 };
 
-template<typename Ctx, typename S, typename T>
-class ast2ast_trail : public trail<Ctx> {
+template<typename S, typename T>
+class ast2ast_trail : public trail {
     ast2ast_trailmap<S,T>& m_map;
 public:
     ast2ast_trail(ast2ast_trailmap<S,T>& m, S* s, T* t) : 
@@ -65,7 +65,7 @@ public:
         m.insert(s,t);
     }
 
-    void undo(Ctx& ctx) override {
+    void undo() override {
         m_map.pop();
     }    
 };
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 9eb90b0ba..adb171d19 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -74,7 +74,7 @@ namespace euf {
     
     class egraph {        
 
-        typedef ptr_vector<trail<egraph> > trail_stack;
+        typedef ptr_vector<trail> trail_stack;
 
         struct to_merge {
             enode* a, * b;
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 8495dd9ab..ed9183e1d 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -148,36 +148,37 @@ namespace datalog {
     //
     // -----------------------------------
 
-    class context::restore_rules : public trail<context> {
+    class context::restore_rules : public trail {
+        context& ctx;
         rule_set* m_old_rules;
         void reset() {
             dealloc(m_old_rules);
             m_old_rules = nullptr;
         }
     public:
-        restore_rules(rule_set& r): m_old_rules(alloc(rule_set, r)) {}
+        restore_rules(context& ctx, rule_set& r): ctx(ctx), m_old_rules(alloc(rule_set, r)) {}
 
         ~restore_rules() override {}
 
-        void undo(context& ctx) override {
+        void undo() override {
             ctx.replace_rules(*m_old_rules);
             reset();
         }
     };
 
     template<typename Ctx, typename Vec>
-    class restore_vec_size_trail : public trail<Ctx> {
+    class restore_vec_size_trail : public trail {
         Vec& m_vector;
         unsigned m_old_size;
     public:
         restore_vec_size_trail(Vec& v): m_vector(v), m_old_size(v.size()) {}
         ~restore_vec_size_trail() override {}
-        void undo(Ctx& ctx) override { m_vector.shrink(m_old_size); }
+        void undo() override { m_vector.shrink(m_old_size); }
     };
 
     void context::push() {
         m_trail.push_scope();
-        m_trail.push(restore_rules(m_rule_set));
+        m_trail.push(restore_rules(*this, m_rule_set));
         m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_rule_fmls));
         m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background));
     }
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 5595923b5..94efa5de2 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -99,7 +99,7 @@ struct dl_context {
     void register_predicate(func_decl* pred, unsigned num_kinds, symbol const* kinds) {
         if (m_collected_cmds) {
             m_collected_cmds->m_rels.push_back(pred);
-            m_trail.push(push_back_vector<dl_context, func_decl_ref_vector>(m_collected_cmds->m_rels));
+            m_trail.push(push_back_vector<func_decl_ref_vector>(m_collected_cmds->m_rels));
         }
         dlctx().register_predicate(pred, false);
         dlctx().set_predicate_representation(pred, num_kinds, kinds);
@@ -111,8 +111,8 @@ struct dl_context {
             expr_ref rl = m_context->bind_vars(rule, true);
             m_collected_cmds->m_rules.push_back(rl);
             m_collected_cmds->m_names.push_back(name);
-            m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_rules));
-            m_trail.push(push_back_vector<dl_context, svector<symbol> >(m_collected_cmds->m_names));
+            m_trail.push(push_back_vector<expr_ref_vector>(m_collected_cmds->m_rules));
+            m_trail.push(push_back_vector<svector<symbol> >(m_collected_cmds->m_names));
         }
         else {
         m_context->add_rule(rule, name, bound);
@@ -130,7 +130,7 @@ struct dl_context {
             qr = m.mk_app(q, args.size(), args.c_ptr());
             qr = m_context->bind_vars(qr, false);
             m_collected_cmds->m_queries.push_back(qr);
-            m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_queries));
+            m_trail.push(push_back_vector<expr_ref_vector>(m_collected_cmds->m_queries));
             return true;
         }
         else {
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 4199265f5..d9f036ffd 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1310,7 +1310,7 @@ namespace qe {
     typedef ref_vector_ptr_hash<expr, ast_manager> expr_ref_vector_hash;
     typedef ref_vector_ptr_eq<expr, ast_manager>   expr_ref_vector_eq;
     typedef hashtable<expr_ref_vector*, expr_ref_vector_hash, expr_ref_vector_eq> clause_table;
-    typedef value_trail<smt::context, unsigned> _value_trail;
+    typedef value_trail<unsigned> _value_trail;
 
 
     class quant_elim_plugin : public i_solver_context {
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 308ca6e98..c94b13e8c 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -47,7 +47,7 @@ namespace arith {
             get_one(false);
             get_zero(true);
             get_zero(false);
-            ctx.push(value_trail<euf::solver, bool>(m_internalize_initialized));
+            ctx.push(value_trail<bool>(m_internalize_initialized));
             m_internalize_initialized = true;
         }
     }
@@ -89,7 +89,7 @@ namespace arith {
     }
 
     void solver::found_unsupported(expr* n) {
-        ctx.push(value_trail<euf::solver, expr*>(m_not_handled));
+        ctx.push(value_trail<expr*>(m_not_handled));
         TRACE("arith", tout << "unsupported " << mk_pp(n, m) << "\n";);
         m_not_handled = n;
     }
@@ -125,7 +125,7 @@ namespace arith {
         if (var != UINT_MAX) {
             return var;
         }
-        ctx.push(value_trail<euf::solver, lpvar>(var));
+        ctx.push(value_trail<lpvar>(var));
         app_ref cnst(a.mk_numeral(rational(c), is_int), m);
         mk_enode(cnst);
         theory_var v = mk_evar(cnst);
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 423f719f2..0a3de5393 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -423,7 +423,7 @@ namespace arith {
             if (b.first == UINT_MAX || (is_lower ? b.second < v : b.second > v)) {
                 TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";);
                 m_history.push_back(vec[ti]);
-                ctx.push(history_trail<euf::solver, constraint_bound>(vec, ti, m_history));
+                ctx.push(history_trail<constraint_bound>(vec, ti, m_history));
                 b.first = ci;
                 b.second = v;
             }
@@ -765,7 +765,7 @@ namespace arith {
 
     void solver::updt_unassigned_bounds(theory_var v, int inc) {
         TRACE("arith_verbose", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";);
-        ctx.push(vector_value_trail<euf::solver, unsigned, false>(m_unassigned_bounds, v));
+        ctx.push(vector_value_trail<unsigned, false>(m_unassigned_bounds, v));
         m_unassigned_bounds[v] += inc;
     }
 
@@ -792,7 +792,7 @@ namespace arith {
     void solver::init_model() {
         if (m.inc() && m_solver.get() && get_num_vars() > 0) {
             TRACE("arith", display(tout << "update variable values\n"););
-            ctx.push(value_trail<euf::solver, bool>(m_model_is_initialized));
+            ctx.push(value_trail<bool>(m_model_is_initialized));
             m_model_is_initialized = true;
             lp().init_model();
         }
@@ -895,7 +895,7 @@ namespace arith {
         }
 
         if (m_assume_eq_candidates.size() > old_sz)
-            ctx.push(restore_size_trail<euf::solver, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
+            ctx.push(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
 
         return delayed_assume_eqs();
     }
@@ -904,7 +904,7 @@ namespace arith {
         if (m_assume_eq_head == m_assume_eq_candidates.size())
             return false;
 
-        ctx.push(value_trail<euf::solver, unsigned>(m_assume_eq_head));
+        ctx.push(value_trail<unsigned>(m_assume_eq_head));
         while (m_assume_eq_head < m_assume_eq_candidates.size()) {
             std::pair<theory_var, theory_var> const& p = m_assume_eq_candidates[m_assume_eq_head];
             theory_var v1 = p.first;
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 4f26af02e..dbe66a4aa 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -28,14 +28,14 @@ namespace array {
         if (m_axioms.contains(idx))
             m_axiom_trail.pop_back();
         else
-            ctx.push(push_back_vector<euf::solver, svector<axiom_record>>(m_axiom_trail));
+            ctx.push(push_back_vector<svector<axiom_record>>(m_axiom_trail));
     }
 
     bool solver::propagate_axiom(unsigned idx) {
         if (m_axioms.contains(idx))
             return false;
         m_axioms.insert(idx);
-        ctx.push(insert_map<euf::solver, axiom_table_t, unsigned>(m_axioms, idx));
+        ctx.push(insert_map<axiom_table_t, unsigned>(m_axioms, idx));
         return assert_axiom(idx);
     }
 
@@ -75,11 +75,11 @@ namespace array {
             return false;                
     }
 
-    struct solver::set_delay_bit : trail<euf::solver> {
+    struct solver::set_delay_bit : trail {
         solver& s;
         unsigned m_idx;
         set_delay_bit(solver& s, unsigned idx) : s(s), m_idx(idx) {}
-        void undo(euf::solver& euf) override {
+        void undo(/*euf::solver& euf*/) override {
             s.m_axiom_trail[m_idx].m_delayed = false;
         }
     };
@@ -458,11 +458,11 @@ namespace array {
         func_decl* diag = nullptr;
         if (!m_sort2epsilon.find(s, eps)) {
             eps = m.mk_fresh_const("epsilon", s);
-            ctx.push(ast2ast_trail<euf::solver, sort, app>(m_sort2epsilon, s, eps));
+            ctx.push(ast2ast_trail<sort, app>(m_sort2epsilon, s, eps));
         }
         if (!m_sort2diag.find(s, diag)) {
             diag = m.mk_fresh_func_decl("diag", 1, &s, s);
-            ctx.push(ast2ast_trail<euf::solver, sort, func_decl>(m_sort2diag, s, diag));
+            ctx.push(ast2ast_trail<sort, func_decl>(m_sort2diag, s, diag));
         }
         return std::make_pair(eps, diag);
     }
diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 3e2ca6cd8..9d5476e31 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -210,8 +210,8 @@ namespace array {
         for (unsigned i = 0; i < dimension; ++i) 
             result->push_back(a.mk_array_ext(s, i));
         m_sort2diff.insert(s, result);
-        ctx.push(insert_map<euf::solver, obj_map<sort, func_decl_ref_vector*>, sort*>(m_sort2diff, s));
-        ctx.push(new_obj_trail<euf::solver,func_decl_ref_vector>(result));
+        ctx.push(insert_map<obj_map<sort, func_decl_ref_vector*>, sort*>(m_sort2diff, s));
+        ctx.push(new_obj_trail<func_decl_ref_vector>(result));
         return *result;
     }
 
diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index c90e14491..78e2bda79 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -176,7 +176,7 @@ namespace array {
             return false;
         force_push();
         bool prop = false;
-        ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
+        ctx.push(value_trail<unsigned>(m_qhead));
         for (; m_qhead < m_axiom_trail.size() && !s().inconsistent(); ++m_qhead)
             if (propagate_axiom(m_qhead))
                 prop = true;
@@ -269,7 +269,7 @@ namespace array {
         auto& d = get_var_data(find(v));
         if (d.m_prop_upward)
             return;
-        ctx.push(reset_flag_trail<euf::solver>(d.m_prop_upward));
+        ctx.push(reset_flag_trail(d.m_prop_upward));
         d.m_prop_upward = true;
         if (should_prop_upward(d))
             propagate_parent_select_axioms(v);
diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
index 24d1b28b6..5c0061019 100644
--- a/src/sat/smt/bv_delay_internalize.cpp
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -345,9 +345,9 @@ namespace bv {
 
     void solver::set_delay_internalize(expr* e, internalize_mode mode) {
         if (!m_delay_internalize.contains(e))
-            ctx.push(insert_obj_map<euf::solver, expr, internalize_mode>(m_delay_internalize, e));
+            ctx.push(insert_obj_map<expr, internalize_mode>(m_delay_internalize, e));
         else 
-            ctx.push(remove_obj_map<euf::solver, expr, internalize_mode>(m_delay_internalize, e, m_delay_internalize[e]));
+            ctx.push(remove_obj_map<expr, internalize_mode>(m_delay_internalize, e, m_delay_internalize[e]));
         m_delay_internalize.insert(e, mode);
     }
 
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 4fe50959c..893d3c616 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -23,21 +23,21 @@ Author:
 
 namespace bv {
 
-    class solver::add_var_pos_trail : public trail<euf::solver> {
+    class solver::add_var_pos_trail : public trail {
         solver::atom* m_atom;
     public:
         add_var_pos_trail(solver::atom* a) :m_atom(a) {}
-        void undo(euf::solver& euf) override {
+        void undo() override {
             SASSERT(m_atom->m_occs);
             m_atom->m_occs = m_atom->m_occs->m_next;
         }
     };
 
-    class solver::add_eq_occurs_trail : public trail<euf::solver> {
+    class solver::add_eq_occurs_trail : public trail {
         atom* m_atom;
     public:
         add_eq_occurs_trail(atom* a) :m_atom(a) {}
-        void undo(euf::solver& euf) override {
+        void undo() override {
             SASSERT(m_atom->m_eqs);
             m_atom->m_eqs = m_atom->m_eqs->m_next;
             if (m_atom->m_eqs)  
@@ -45,12 +45,12 @@ namespace bv {
         }
     };    
 
-    class solver::del_eq_occurs_trail : public trail<euf::solver> {
+    class solver::del_eq_occurs_trail : public trail {
         atom* m_atom;
         eq_occurs* m_node;
     public:
         del_eq_occurs_trail(atom* a, eq_occurs* n) : m_atom(a), m_node(n) {}
-        void undo(euf::solver& euf) override {
+        void undo() override {
             if (m_node->m_next)
                 m_node->m_next->m_prev = m_node;
             if (m_node->m_prev) 
@@ -71,12 +71,12 @@ namespace bv {
         ctx.push(del_eq_occurs_trail(a, occ));
     }
 
-    class solver::mk_atom_trail : public trail<euf::solver> {
+    class solver::mk_atom_trail : public trail {
         solver& th;
         sat::bool_var m_var;
     public:
         mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {}
-        void undo(euf::solver& euf) override {
+        void undo() override {
             solver::atom* a = th.get_bv2a(m_var);
             a->~atom();
             th.erase_bv2a(m_var);
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 99ac940e8..878ecbe66 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -24,7 +24,7 @@ Author:
 
 namespace bv {
 
-    class solver::bit_trail : public trail<euf::solver> {
+    class solver::bit_trail : public trail {
         solver& s;
         solver::var_pos vp;
         sat::literal lit;
@@ -36,14 +36,14 @@ namespace bv {
         }
     };
 
-    class solver::bit_occs_trail : public trail<euf::solver> {
+    class solver::bit_occs_trail : public trail {
         atom& a;
         var_pos_occ* m_occs;
 
     public:
         bit_occs_trail(solver& s, atom& a): a(a), m_occs(a.m_occs) {}
         
-        virtual void undo(euf::solver& euf) {
+        virtual void undo() {
             a.m_occs = m_occs;
         }
     };
@@ -413,7 +413,7 @@ namespace bv {
         if (m_prop_queue_head == m_prop_queue.size())
             return false;
         force_push();
-        ctx.push(value_trail<euf::solver, unsigned>(m_prop_queue_head));
+        ctx.push(value_trail<unsigned>(m_prop_queue_head));
         for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
             auto const p = m_prop_queue[m_prop_queue_head];
             if (p.m_atom) {
@@ -559,7 +559,7 @@ namespace bv {
             SASSERT(l2.var() == l.var());
             VERIFY(l2.var() == l.var());
             sat::literal r2 = (l.sign() == l2.sign()) ? r : ~r;
-            ctx.push(vector2_value_trail<euf::solver, bits_vector, sat::literal>(m_bits, vp.first, vp.second));
+            ctx.push(vector2_value_trail<bits_vector, sat::literal>(m_bits, vp.first, vp.second));
             m_bits[vp.first][vp.second] = r2;
             set_bit_eh(vp.first, r2, vp.second);
         }
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 78ebf32f0..e7f88bf2e 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -372,7 +372,7 @@ namespace dt {
             }
             SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr));
             d->m_recognizers[c_idx] = recognizer;
-            ctx.push(set_vector_idx_trail<euf::solver, enode>(d->m_recognizers, c_idx));
+            ctx.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
             if (val == l_false)
                 propagate_recognizer(v, recognizer);
         }
@@ -455,7 +455,7 @@ namespace dt {
         auto* con2 = d2->m_constructor;
         if (con2 != nullptr) {
             if (con1 == nullptr) {
-                ctx.push(set_ptr_trail<euf::solver, enode>(con1));
+                ctx.push(set_ptr_trail<enode>(con1));
                 // check whether there is a recognizer in d1 that conflicts with con2;
                 if (!d1->m_recognizers.empty()) {
                     unsigned c_idx = dt.get_constructor_idx(con2->get_decl());
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 26f8bee23..9f8339e0d 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -42,7 +42,7 @@ namespace euf {
                 get_drat().def_add_arg(arg->get_id());
             get_drat().def_end();
             m_drat_asts.insert(e);
-            push(insert_obj_trail<solver, ast>(m_drat_asts, e));
+            push(insert_obj_trail<ast>(m_drat_asts, e));
         }
         else {
             IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
@@ -82,7 +82,7 @@ namespace euf {
         if (m_drat_asts.contains(f))
             return;
         m_drat_asts.insert(f);
-        push(insert_obj_trail<solver, ast>(m_drat_asts, f));
+        push(insert_obj_trail< ast>(m_drat_asts, f));
         std::ostringstream strm;
         smt2_pp_environment_dbg env(m);
         ast_smt2_pp(strm, f, env);
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 6658caf6c..f86102fe8 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -141,7 +141,7 @@ namespace euf {
         if (m.is_model_value(f))
             return;
         m_unhandled_functions.push_back(f);
-        m_trail.push(push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions));
+        m_trail.push(push_back_vector<func_decl_ref_vector>(m_unhandled_functions));
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
     }
 
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index ab3a2ac7c..2f38c7638 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -247,12 +247,12 @@ namespace euf {
         template <typename V>
         void push_vec(ptr_vector<V>& vec, V* val) {
             vec.push_back(val);
-            push(push_back_trail<solver, V*, false>(vec));
+            push(push_back_trail< V*, false>(vec));
         }
         template <typename V>
         void push_vec(svector<V>& vec, V val) {
             vec.push_back(val);
-            push(push_back_trail<solver, V, false>(vec));
+            push(push_back_trail< V, false>(vec));
         }
         euf_trail_stack& get_trail_stack() { return m_trail; }
 
diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index cbf767fc2..80c4f6e0e 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -64,7 +64,7 @@ namespace fpa {
             m.inc_ref(e);
             m.inc_ref(res);
 
-            ctx.push(insert_ref2_map<euf::solver, ast_manager, expr, expr>(m, m_conversions, e, res.get()));
+            ctx.push(insert_ref2_map<ast_manager, expr, expr>(m, m_conversions, e, res.get()));
         }
         return res;
     }
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index fef462b70..e69eb3cf2 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -120,12 +120,12 @@ namespace q {
         return out;
     }
 
-    struct restore_watch : public trail<euf::solver> {
+    struct restore_watch : public trail {
         vector<unsigned_vector>& v;
         unsigned idx, offset;
         restore_watch(vector<unsigned_vector>& v, unsigned idx):
             v(v), idx(idx), offset(v[idx].size()) {}
-        void undo(euf::solver& ctx) override {
+        void undo() override {
             v[idx].shrink(offset);
         }
     };
@@ -191,20 +191,20 @@ namespace q {
         }
     }
 
-    struct ematch::remove_binding : public trail<euf::solver> {
+    struct ematch::remove_binding : public trail {
         clause& c;
         binding* b;
         remove_binding(clause& c, binding* b): c(c), b(b) {}
-        void undo(euf::solver& ctx) override {
+        void undo() override {
             binding::remove_from(c.m_bindings, b);
         }        
     };
 
-    struct ematch::insert_binding : public trail<euf::solver> {
+    struct ematch::insert_binding : public trail {
         clause& c;
         binding* b;
         insert_binding(clause& c, binding* b): c(c), b(b) {}
-        void undo(euf::solver& ctx) override {
+        void undo() override {
             binding::push_to_front(c.m_bindings, b);
         }
     };
@@ -306,7 +306,7 @@ namespace q {
             return nullptr;
         fingerprint* f = new (ctx.get_region()) fingerprint(c, b, max_generation);
         m_fingerprints.insert(f);
-        ctx.push(insert_map<euf::solver, fingerprints, fingerprint*>(m_fingerprints, f));
+        ctx.push(insert_map<fingerprints, fingerprint*>(m_fingerprints, f));
         return f;
     }
 
@@ -328,11 +328,11 @@ namespace q {
         return l.sign ? ~ctx.mk_literal(fml) : ctx.mk_literal(fml);
     }
 
-    struct ematch::reset_in_queue : public trail<euf::solver> {
+    struct ematch::reset_in_queue : public trail {
         ematch& e;
         reset_in_queue(ematch& e) :e(e) {}
 
-        void undo(euf::solver& ctx) override {
+        void undo() override {
             e.m_node_in_queue.reset();
             e.m_clause_in_queue.reset();
             e.m_in_queue_set = false;
@@ -362,7 +362,7 @@ namespace q {
         if (!m_clause_in_queue.contains(idx)) {
             m_clause_in_queue.insert(idx);
             m_clause_queue.push_back(idx);
-            ctx.push(push_back_vector<euf::solver, unsigned_vector>(m_clause_queue));
+            ctx.push(push_back_vector<unsigned_vector>(m_clause_queue));
         }
     }
 
@@ -418,10 +418,10 @@ namespace q {
         }
     }
 
-    struct ematch::pop_clause : public trail<euf::solver> {
+    struct ematch::pop_clause : public trail {
         ematch& em;
         pop_clause(ematch& em): em(em) {}
-        void undo(euf::solver& ctx) override {
+        void undo() override {
             em.m_q2clauses.remove(em.m_clauses.back()->q());
             dealloc(em.m_clauses.back());
             em.m_clauses.pop_back();
@@ -472,7 +472,7 @@ namespace q {
         bool propagated = false;
         if (m_qhead >= m_clause_queue.size())
             return m_inst_queue.propagate();
-        ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
+        ctx.push(value_trail<unsigned>(m_qhead));
         ptr_buffer<binding> to_remove;
         for (; m_qhead < m_clause_queue.size(); ++m_qhead) {
             unsigned idx = m_clause_queue[m_qhead];
diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index 53953398f..42af24de8 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -75,9 +75,9 @@ namespace q {
 
 
     template<typename T>
-    class mam_value_trail : public value_trail<euf::solver, T> {
+    class mam_value_trail : public value_trail<T> {
     public:
-        mam_value_trail(T & value):value_trail<euf::solver, T>(value) {}
+        mam_value_trail(T & value):value_trail<T>(value) {}
     };
 
     unsigned get_max_generation(unsigned n, enode* const* nodes) {
@@ -2812,12 +2812,12 @@ namespace q {
         egraph *                   m_egraph;
 #endif
 
-        class mk_tree_trail : public trail<euf::solver> {
+        class mk_tree_trail : public trail {
             ptr_vector<code_tree> & m_trees;
             unsigned                m_lbl_id;
         public:
             mk_tree_trail(ptr_vector<code_tree> & t, unsigned id):m_trees(t), m_lbl_id(id) {}
-            void undo(euf::solver & m) override {
+            void undo() override {
                 dealloc(m_trees[m_lbl_id]);
                 m_trees[m_lbl_id] = nullptr;
             }
@@ -2871,7 +2871,7 @@ namespace q {
                 }
             }
             DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp);
-                       ctx.push(push_back_trail<euf::solver, app*, false>(m_trees[lbl_id]->get_patterns())););
+                       ctx.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns())););
             TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
         }
 
@@ -3067,11 +3067,11 @@ namespace q {
         enode *                     m_other { nullptr }; // temp field
         bool                        m_check_missing_instances { false };
 
-        class reset_to_match : public trail<euf::solver> {
+        class reset_to_match : public trail {
             mam_impl& i;
         public:
             reset_to_match(mam_impl& i):i(i) {}
-            void undo(euf::solver& ctx) override {
+            void undo() override {
                 if (i.m_to_match.empty())
                     return;
                 for (code_tree* t : i.m_to_match) 
@@ -3080,11 +3080,11 @@ namespace q {
             }
         };
         
-        class reset_new_patterns : public trail<euf::solver> {
+        class reset_new_patterns : public trail {
             mam_impl& i;
         public:
             reset_new_patterns(mam_impl& i):i(i) {}
-            void undo(euf::solver& ctx) override {
+            void undo() override {
                 i.m_new_patterns.reset();
             }
         };
@@ -3139,7 +3139,7 @@ namespace q {
             TRACE("mam_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";);
             if (m_is_clbl[lbl_id])
                 return;
-            ctx.push(set_bitvector_trail<euf::solver>(m_is_clbl, lbl_id));
+            ctx.push(set_bitvector_trail(m_is_clbl, lbl_id));
             SASSERT(m_is_clbl[lbl_id]);
             unsigned h = m_lbl_hasher(lbl);
             for (enode* app : m_egraph.enodes_of(lbl)) {
@@ -3180,7 +3180,7 @@ namespace q {
             TRACE("mam_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << "\n";);
             if (m_is_plbl[lbl_id])
                 return;
-            ctx.push(set_bitvector_trail<euf::solver>(m_is_plbl, lbl_id));
+            ctx.push(set_bitvector_trail(m_is_plbl, lbl_id));
             SASSERT(m_is_plbl[lbl_id]);
             SASSERT(is_plbl(lbl));
             unsigned h = m_lbl_hasher(lbl);
@@ -3227,7 +3227,7 @@ namespace q {
                 p = p->m_child;
             }
             curr->m_code = mk_code(qa, mp, pat_idx);
-            ctx.push(new_obj_trail<euf::solver, code_tree>(curr->m_code));
+            ctx.push(new_obj_trail<code_tree>(curr->m_code));
             return head;
         }
 
@@ -3250,7 +3250,7 @@ namespace q {
                                 insert_code(t, qa, mp, p->m_pattern_idx);
                             }
                             else {
-                                ctx.push(set_ptr_trail<euf::solver, path_tree>(t->m_first_child));
+                                ctx.push(set_ptr_trail<path_tree>(t->m_first_child));
                                 t->m_first_child = mk_path_tree(p->m_child, qa, mp);
                             }
                         }
@@ -3260,9 +3260,9 @@ namespace q {
                                     insert_code(t, qa, mp, p->m_pattern_idx);
                                 }
                                 else {
-                                    ctx.push(set_ptr_trail<euf::solver, code_tree>(t->m_code));
+                                    ctx.push(set_ptr_trail<code_tree>(t->m_code));
                                     t->m_code = mk_code(qa, mp, p->m_pattern_idx);
-                                    ctx.push(new_obj_trail<euf::solver, code_tree>(t->m_code));
+                                    ctx.push(new_obj_trail<code_tree>(t->m_code));
                                 }
                             }
                             else {
@@ -3275,10 +3275,10 @@ namespace q {
                 prev_sibling = t;
                 t = t->m_sibling;
             }
-            ctx.push(set_ptr_trail<euf::solver, path_tree>(prev_sibling->m_sibling));
+            ctx.push(set_ptr_trail<path_tree>(prev_sibling->m_sibling));
             prev_sibling->m_sibling = mk_path_tree(p, qa, mp);
             if (!found_label) {
-                ctx.push(value_trail<euf::solver, approx_set>(head->m_filter));
+                ctx.push(value_trail<approx_set>(head->m_filter));
                 head->m_filter.insert(m_lbl_hasher(p->m_label));
             }
         }
@@ -3288,7 +3288,7 @@ namespace q {
                 insert(m_pc[h1][h2], p, qa, mp);
             }
             else {
-                ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pc[h1][h2]));
+                ctx.push(set_ptr_trail<path_tree>(m_pc[h1][h2]));
                 m_pc[h1][h2] = mk_path_tree(p, qa, mp);
             }
             TRACE("mam_path_tree_updt",
@@ -3305,7 +3305,7 @@ namespace q {
                         insert(m_pp[h1][h2].first, p2, qa, mp);
                 }
                 else {
-                    ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pp[h1][h2].first));
+                    ctx.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
                     m_pp[h1][h2].first = mk_path_tree(p1, qa, mp);
                     insert(m_pp[h1][h2].first, p2, qa, mp);
                 }
@@ -3323,8 +3323,8 @@ namespace q {
                 }
                 else {
                     SASSERT(m_pp[h1][h2].second == nullptr);
-                    ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pp[h1][h2].first));
-                    ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pp[h1][h2].second));
+                    ctx.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
+                    ctx.push(set_ptr_trail<path_tree>(m_pp[h1][h2].second));
                     m_pp[h1][h2].first  = mk_path_tree(p1, qa, mp);
                     m_pp[h1][h2].second = mk_path_tree(p2, qa, mp);
                 }
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index f674c64fc..32420a7bf 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -247,8 +247,8 @@ namespace q {
             var_subst subst(m);
             result = alloc(q_body, m);
             m_q2body.insert(q, result);
-            ctx.push(new_obj_trail<euf::solver, q_body>(result));
-            ctx.push(insert_obj_map<euf::solver, quantifier, q_body*>(m_q2body, q));
+            ctx.push(new_obj_trail<q_body>(result));
+            ctx.push(insert_obj_map<quantifier, q_body*>(m_q2body, q));
             app_ref_vector& vars = result->vars;
             vars.resize(sz, nullptr);
             for (unsigned i = 0; i < sz; ++i) {
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index 4d5a1a275..3d2a06629 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -98,8 +98,8 @@ namespace q {
         if (!m_q2info.find(q, info)) {
             info = alloc(quantifier_macro_info, m, m_qs.flatten(q));
             m_q2info.insert(q, info);
-            ctx.push(new_obj_trail<euf::solver, quantifier_macro_info>(info));
-            ctx.push(insert_obj_map<euf::solver, quantifier, quantifier_macro_info*>(m_q2info, q));
+            ctx.push(new_obj_trail<quantifier_macro_info>(info));
+            ctx.push(insert_obj_map<quantifier, quantifier_macro_info*>(m_q2info, q));
         }
         return info;
     }
@@ -200,8 +200,8 @@ namespace q {
         if (!proj)
             return nullptr;
         m_projections.insert(srt, proj);
-        ctx.push(new_obj_trail<euf::solver, projection_function>(proj));
-        ctx.push(insert_obj_map<euf::solver, sort, projection_function*>(m_projections, srt));
+        ctx.push(new_obj_trail<projection_function>(proj));
+        ctx.push(insert_obj_map<sort, projection_function*>(m_projections, srt));
         return proj;
     }
 
diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp
index fc1a5249f..96eee11c7 100644
--- a/src/sat/smt/q_queue.cpp
+++ b/src/sat/smt/q_queue.cpp
@@ -121,10 +121,10 @@ namespace q {
         return std::max(f.m_max_generation + 1, static_cast<unsigned>(r));
     }
 
-    struct queue::reset_new_entries : public trail<euf::solver> {
+    struct queue::reset_new_entries : public trail {
         svector<entry>& m_entries;
         reset_new_entries(svector<entry>& e): m_entries(e) {}
-        void undo(euf::solver& ctx) override {
+        void undo() override {
             m_entries.reset();
         }
     };
@@ -189,18 +189,18 @@ namespace q {
             else {
                 TRACE("q", tout << "delaying quantifier instantiation... " << f << "\n" << mk_pp(f.q(), m) << "\ncost: " << curr.m_cost << "\n";);
                 m_delayed_entries.push_back(curr);
-                ctx.push(push_back_vector<euf::solver,svector<entry>>(m_delayed_entries));
+                ctx.push(push_back_vector<svector<entry>>(m_delayed_entries));
             }
         }
         m_new_entries.reset();
         return true;
     }    
 
-    struct queue::reset_instantiated : public trail<euf::solver> {
+    struct queue::reset_instantiated : public trail {
         queue& q;
         unsigned idx;
         reset_instantiated(queue& q, unsigned idx): q(q), idx(idx) {}
-        void undo(euf::solver& ctx) override {
+        void undo() override {
             q.m_delayed_entries[idx].m_instantiated = false;
         }
     };
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 8a52d92b7..c2139993e 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -173,7 +173,7 @@ namespace q {
         m.inc_ref(q_flat);
         m.inc_ref(q);
         m_flat.insert(q, q_flat);
-        ctx.push(insert_ref2_map<euf::solver, ast_manager, quantifier, quantifier>(m, m_flat, q, q_flat));
+        ctx.push(insert_ref2_map<ast_manager, quantifier, quantifier>(m, m_flat, q, q_flat));
         return q_flat;
     }
 
@@ -188,7 +188,7 @@ namespace q {
             if (m_unit_table.contains(s))
                 continue;
             m_unit_table.insert(s, e);
-            ctx.push(insert_map<euf::solver, obj_map<sort, expr*>, sort*>(m_unit_table, s));
+            ctx.push(insert_map<obj_map<sort, expr*>, sort*>(m_unit_table, s));
         }
     }
 
@@ -203,7 +203,7 @@ namespace q {
         expr* val = mdl.get_some_value(s);
         m.inc_ref(val);
         m.inc_ref(s);
-        ctx.push(insert_ref2_map<euf::solver, ast_manager, sort, expr>(m, m_unit_table, s, val));
+        ctx.push(insert_ref2_map<ast_manager, sort, expr>(m, m_unit_table, s, val));
         return val;
     }
 
diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp
index fb67f7e90..8190e3bf7 100644
--- a/src/sat/smt/user_solver.cpp
+++ b/src/sat/smt/user_solver.cpp
@@ -92,7 +92,7 @@ namespace user {
         if (m_qhead == m_prop.size())
             return false;
         force_push();
-        ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
+        ctx.push(value_trail<unsigned>(m_qhead));
         unsigned np = m_stats.m_num_propagations;
         for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) {
             auto const& prop = m_prop[m_qhead];
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index b8051ff3d..de328a242 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -26,7 +26,7 @@ Revision History:
 
 namespace smt {
 
-    class already_processed_trail : public trail<context> {
+    class already_processed_trail : public trail {
         // Remark: it is safer to use a trail object, because it guarantees that the enodes
         // are still alive when the undo operation is performed.
         //
@@ -42,7 +42,7 @@ namespace smt {
             m_n2(n2) {
         }
         
-        void undo(context & ctx) override {
+        void undo() override {
             m_already_processed.erase(m_n1, m_n2);
             TRACE("arith_eq_adapter_profile", tout << "del #" << m_n1->get_owner_id() << " #" << m_n2->get_owner_id() << "\n";);
         }
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 3090bd7e2..30b3fcee4 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -66,12 +66,12 @@ namespace {
 
     typedef trail_stack<mam_impl> mam_trail_stack;
 
-    typedef trail<mam_impl> mam_trail;
+    typedef trail mam_trail;
 
     template<typename T>
-    class mam_value_trail : public value_trail<mam_impl, T> {
+    class mam_value_trail : public value_trail<T> {
     public:
-        mam_value_trail(T & value):value_trail<mam_impl, T>(value) {}
+        mam_value_trail(T & value):value_trail<T>(value) {}
     };
 
 
@@ -2883,7 +2883,7 @@ namespace {
             unsigned                m_lbl_id;
         public:
             mk_tree_trail(ptr_vector<code_tree> & t, unsigned id):m_trees(t), m_lbl_id(id) {}
-            void undo(mam_impl & m) override {
+            void undo() override {
                 dealloc(m_trees[m_lbl_id]);
                 m_trees[m_lbl_id] = nullptr;
             }
@@ -2936,7 +2936,7 @@ namespace {
                 }
             }
             DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp);
-                       m_trail_stack.push(push_back_trail<mam_impl, app*, false>(m_trees[lbl_id]->get_patterns())););
+                       m_trail_stack.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns())););
             TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
         }
 
@@ -3140,10 +3140,11 @@ namespace {
         friend class add_shared_enode_trail;
 
         class add_shared_enode_trail : public mam_trail {
+            mam_impl& m;
             enode * m_enode;
         public:
-            add_shared_enode_trail(enode * n):m_enode(n) {}
-            void undo(mam_impl & m) override { m.m_shared_enodes.erase(m_enode); }
+            add_shared_enode_trail(mam_impl& m, enode * n):m(m), m_enode(n) {}
+            void undo() override { m.m_shared_enodes.erase(m_enode); }
         };
 
 #ifdef Z3DEBUG
@@ -3198,7 +3199,7 @@ namespace {
             TRACE("mam_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";);
             if (m_is_clbl[lbl_id])
                 return;
-            m_trail_stack.push(set_bitvector_trail<mam_impl>(m_is_clbl, lbl_id));
+            m_trail_stack.push(set_bitvector_trail(m_is_clbl, lbl_id));
             SASSERT(m_is_clbl[lbl_id]);
             unsigned h = m_lbl_hasher(lbl);
             for (enode* app : m_context.enodes_of(lbl)) {
@@ -3239,7 +3240,7 @@ namespace {
             TRACE("mam_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << "\n";);
             if (m_is_plbl[lbl_id])
                 return;
-            m_trail_stack.push(set_bitvector_trail<mam_impl>(m_is_plbl, lbl_id));
+            m_trail_stack.push(set_bitvector_trail(m_is_plbl, lbl_id));
             SASSERT(m_is_plbl[lbl_id]);
             SASSERT(is_plbl(lbl));
             unsigned h = m_lbl_hasher(lbl);
@@ -3286,7 +3287,7 @@ namespace {
                 p = p->m_child;
             }
             curr->m_code = mk_code(qa, mp, pat_idx);
-            m_trail_stack.push(new_obj_trail<mam_impl, code_tree>(curr->m_code));
+            m_trail_stack.push(new_obj_trail<code_tree>(curr->m_code));
             return head;
         }
 
@@ -3309,7 +3310,7 @@ namespace {
                                 insert_code(t, qa, mp, p->m_pattern_idx);
                             }
                             else {
-                                m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(t->m_first_child));
+                                m_trail_stack.push(set_ptr_trail<path_tree>(t->m_first_child));
                                 t->m_first_child = mk_path_tree(p->m_child, qa, mp);
                             }
                         }
@@ -3319,9 +3320,9 @@ namespace {
                                     insert_code(t, qa, mp, p->m_pattern_idx);
                                 }
                                 else {
-                                    m_trail_stack.push(set_ptr_trail<mam_impl, code_tree>(t->m_code));
+                                    m_trail_stack.push(set_ptr_trail<code_tree>(t->m_code));
                                     t->m_code = mk_code(qa, mp, p->m_pattern_idx);
-                                    m_trail_stack.push(new_obj_trail<mam_impl, code_tree>(t->m_code));
+                                    m_trail_stack.push(new_obj_trail< code_tree>(t->m_code));
                                 }
                             }
                             else {
@@ -3334,10 +3335,10 @@ namespace {
                 prev_sibling = t;
                 t = t->m_sibling;
             }
-            m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(prev_sibling->m_sibling));
+            m_trail_stack.push(set_ptr_trail<path_tree>(prev_sibling->m_sibling));
             prev_sibling->m_sibling = mk_path_tree(p, qa, mp);
             if (!found_label) {
-                m_trail_stack.push(value_trail<mam_impl, approx_set>(head->m_filter));
+                m_trail_stack.push(value_trail<approx_set>(head->m_filter));
                 head->m_filter.insert(m_lbl_hasher(p->m_label));
             }
         }
@@ -3347,7 +3348,7 @@ namespace {
                 insert(m_pc[h1][h2], p, qa, mp);
             }
             else {
-                m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pc[h1][h2]));
+                m_trail_stack.push(set_ptr_trail<path_tree>(m_pc[h1][h2]));
                 m_pc[h1][h2] = mk_path_tree(p, qa, mp);
             }
             TRACE("mam_path_tree_updt",
@@ -3364,7 +3365,7 @@ namespace {
                         insert(m_pp[h1][h2].first, p2, qa, mp);
                 }
                 else {
-                    m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pp[h1][h2].first));
+                    m_trail_stack.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
                     m_pp[h1][h2].first = mk_path_tree(p1, qa, mp);
                     insert(m_pp[h1][h2].first, p2, qa, mp);
                 }
@@ -3382,8 +3383,8 @@ namespace {
                 }
                 else {
                     SASSERT(m_pp[h1][h2].second == 0);
-                    m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pp[h1][h2].first));
-                    m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pp[h1][h2].second));
+                    m_trail_stack.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
+                    m_trail_stack.push(set_ptr_trail<path_tree>(m_pp[h1][h2].second));
                     m_pp[h1][h2].first  = mk_path_tree(p1, qa, mp);
                     m_pp[h1][h2].second = mk_path_tree(p2, qa, mp);
                 }
@@ -3796,7 +3797,7 @@ namespace {
                 todo.pop_back();
                 if (n->is_ground()) {
                     enode * e = mk_enode(m_context, qa, n);
-                    m_trail_stack.push(add_shared_enode_trail(e));
+                    m_trail_stack.push(add_shared_enode_trail(*this, e));
                     m_shared_enodes.insert(e);
                 }
                 else {
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index 3030b54b5..077b342f6 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -719,7 +719,7 @@ void seq_axioms::ensure_digit_axiom() {
             expr_ref cnst(seq.mk_char('0'+i), m);
             add_axiom(mk_eq(m_sk.mk_digit2int(cnst), a.mk_int(i)));
         }
-        ctx().push_trail(value_trail<context, bool>(m_digits_initialized));
+        ctx().push_trail(value_trail<bool>(m_digits_initialized));
         m_digits_initialized = true;
     }
 }
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index cd91b790c..05ca8df7f 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1148,7 +1148,7 @@ bool theory_seq::branch_variable_eq(eq const& e) {
 
 void theory_seq::insert_branch_start(unsigned k, unsigned s) {
     m_branch_start.insert(k, s);
-    m_trail_stack.push(pop_branch(k));
+    m_trail_stack.push(pop_branch(*this, k));
 }
 
 unsigned theory_seq::find_branch_start(unsigned k) {
@@ -1365,7 +1365,7 @@ bool theory_seq::check_length_coherence0(expr* e) {
 
         if (p || assume_equality(e, emp)) {
             if (!ctx.at_base_level()) {
-                m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
+                m_trail_stack.push(push_replay(*this, alloc(replay_length_coherence, m, e)));
             }
             return true;
         }
@@ -1577,12 +1577,12 @@ bool theory_seq::is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector co
     return false;
 }
 
-struct remove_obj_pair_map : public trail<context> {
+struct remove_obj_pair_map : public trail {
     obj_pair_hashtable<expr, expr> & m_map;
     expr* a, *b;
     remove_obj_pair_map(obj_pair_hashtable<expr, expr> & map, expr* a, expr* b):
         m_map(map), a(a), b(b) {}
-    void undo(context& ctx) override {
+    void undo() override {
         m_map.erase(std::make_pair(a, b));
     }
 };
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index bf62acac1..b22c61039 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -379,7 +379,7 @@ namespace smt {
             if (entry.m_re == regex) 
                 continue;
 
-            th.m_trail_stack.push(vector_value_trail<theory_seq, s_in_re, true>(m_s_in_re, i));
+            th.m_trail_stack.push(vector_value_trail<s_in_re, true>(m_s_in_re, i));
             m_s_in_re[i].m_active = false;
             IF_VERBOSE(11, verbose_stream() << "Intersect " << regex << " " << 
                        mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << std::endl;);
@@ -390,7 +390,7 @@ namespace smt {
                 lits.push_back(~th.mk_eq(n1->get_owner(), n2->get_owner(), false));
         }
         m_s_in_re.push_back(s_in_re(lit, s, regex));
-        th.get_trail_stack().push(push_back_vector<theory_seq, vector<s_in_re>>(m_s_in_re));
+        th.get_trail_stack().push(push_back_vector<vector<s_in_re>>(m_s_in_re));
         if (lits.empty())
             return false;
         lits.push_back(~lit);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index a362cc364..66a27b1fb 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -66,19 +66,8 @@ namespace smt {
         m_e_internalized_stack(m),
         m_l_internalized_stack(m),
         m_final_check_idx(0),
-        m_is_auxiliary(false),
-        m_par(nullptr),
-        m_par_index(0),
         m_cg_table(m),
-        m_is_diseq_tmp(nullptr),
         m_units_to_reassert(m),
-        m_qhead(0),
-        m_simp_qhead(0),
-        m_simp_counter(0),
-        m_bvar_inc(1.0),
-        m_phase_cache_on(true),
-        m_phase_counter(0),
-        m_phase_default(false),
         m_conflict(null_b_justification),
         m_not_l(null_literal),
         m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
@@ -86,16 +75,9 @@ namespace smt {
         m_dyn_ack_manager(*this, p),
         m_unknown("unknown"),
         m_unsat_core(m),
-#ifdef Z3DEBUG
-        m_trail_enabled(true),
-#endif
-        m_scope_lvl(0),
-        m_base_lvl(0),
-        m_search_lvl(0),
-        m_generation(0),
-        m_last_search_result(l_undef),
-        m_last_search_failure(UNKNOWN),
-        m_searching(false) {
+        m_mk_bool_var_trail(*this),
+        m_mk_enode_trail(*this),
+        m_mk_lambda_trail(*this) {
 
         SASSERT(m_scope_lvl == 0);
         SASSERT(m_base_lvl == 0);
@@ -447,18 +429,20 @@ namespace smt {
         m_th_diseq_propagation_queue.push_back(new_th_eq(th, lhs, rhs));
     }
 
-    class add_eq_trail : public trail<context> {
+    class add_eq_trail : public trail {
+        context& ctx;
         enode * m_r1;
         enode * m_n1;
         unsigned m_r2_num_parents;
     public:
-        add_eq_trail(enode * r1, enode * n1, unsigned r2_num_parents):
+        add_eq_trail(context& ctx, enode * r1, enode * n1, unsigned r2_num_parents):
+            ctx(ctx),
             m_r1(r1),
             m_n1(n1),
             m_r2_num_parents(r2_num_parents) {
         }
 
-        void undo(context & ctx) override {
+        void undo() override {
             ctx.undo_add_eq(m_r1, m_n1, m_r2_num_parents);
         }
     };
@@ -526,7 +510,7 @@ namespace smt {
                 mark_as_relevant(r1);
             }
 
-            push_trail(add_eq_trail(r1, n1, r2->get_num_parents()));
+            push_trail(add_eq_trail(*this, r1, n1, r2->get_num_parents()));
 
             m_qmanager->add_eq_eh(r1, r2);
 
@@ -1064,7 +1048,7 @@ namespace smt {
               );
 
         DEBUG_CODE(
-            push_trail(push_back_trail<context, enode_pair, false>(m_diseq_vector));
+            push_trail(push_back_trail<enode_pair, false>(m_diseq_vector));
             m_diseq_vector.push_back(enode_pair(n1, n2)););
 
         if (r1 == r2) {
@@ -1379,11 +1363,12 @@ namespace smt {
         return true;
     }
 
-    class set_var_theory_trail : public trail<context> {
+    class set_var_theory_trail : public trail {
+        context& ctx;
         bool_var m_var;
     public:
-        set_var_theory_trail(bool_var v):m_var(v) {}
-        void undo(context & ctx) override {
+        set_var_theory_trail(context& ctx, bool_var v): ctx(ctx), m_var(v) {}
+        void undo() override {
             bool_var_data & d = ctx.m_bdata[m_var];
             d.reset_notify_theory();
         }
@@ -1394,7 +1379,7 @@ namespace smt {
         SASSERT(tid > 0 && tid <= 255);
         SASSERT(get_intern_level(v) <= m_scope_lvl);
         if (m_scope_lvl > get_intern_level(v))
-            push_trail(set_var_theory_trail(v));
+            push_trail(set_var_theory_trail(*this, v));
         bool_var_data & d = m_bdata[v];
         d.set_notify_theory(tid);
     }
@@ -1642,7 +1627,7 @@ namespace smt {
             SASSERT(th);
             th->new_eq_eh(curr.m_lhs, curr.m_rhs);
             DEBUG_CODE(
-                push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_eqs));
+                push_trail(push_back_trail<new_th_eq, false>(m_propagated_th_eqs));
                 m_propagated_th_eqs.push_back(curr););
         }
         m_th_eq_propagation_queue.reset();
@@ -1655,7 +1640,7 @@ namespace smt {
             SASSERT(th);
             th->new_diseq_eh(curr.m_lhs, curr.m_rhs);
             DEBUG_CODE(
-                push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_diseqs));
+                push_trail(push_back_trail<new_th_eq, false>(m_propagated_th_diseqs));
                 m_propagated_th_diseqs.push_back(curr););
         }
         m_th_diseq_propagation_queue.reset();
@@ -2997,13 +2982,15 @@ namespace smt {
         assert_expr_core(e, pr);
     }
 
-    class case_split_insert_trail : public trail<context> {
+    class case_split_insert_trail : public trail {
+        context& ctx;
         literal l;
     public:
-        case_split_insert_trail(literal l):
+        case_split_insert_trail(context& ctx, literal l):
+            ctx(ctx),
             l(l) {
         }
-        void undo(context & ctx) override {
+        void undo() override {
             ctx.undo_th_case_split(l);
         }
     };
@@ -3029,11 +3016,11 @@ namespace smt {
                 literal l = lits[i];
                 SASSERT(!m_all_th_case_split_literals.contains(l.index()));
                 m_all_th_case_split_literals.insert(l.index());
-                push_trail(case_split_insert_trail(l));
+                push_trail(case_split_insert_trail(*this, l));
                 new_case_split.push_back(l);
             }
             m_th_case_split_sets.push_back(new_case_split);
-            push_trail(push_back_vector<context, vector<literal_vector> >(m_th_case_split_sets));
+            push_trail(push_back_vector<vector<literal_vector> >(m_th_case_split_sets));
             for (unsigned i = 0; i < num_lits; ++i) {
                 literal l = lits[i];
                 if (!m_literal2casesplitsets.contains(l.index())) {
@@ -4348,17 +4335,18 @@ namespace smt {
     /**
        \brief Undo object for bool var m_true_first field update.
     */
-    class set_true_first_trail : public trail<context> {
+    class set_true_first_trail : public trail {
+        context& ctx;
         bool_var m_var;
     public:
-        set_true_first_trail(bool_var v):m_var(v) {}
-        void undo(context & ctx) override {
+        set_true_first_trail(context& ctx, bool_var v): ctx(ctx), m_var(v) {}
+        void undo() override {
             ctx.m_bdata[m_var].reset_true_first_flag();
         }
     };
 
     void context::set_true_first_flag(bool_var v) {
-        push_trail(set_true_first_trail(v));
+        push_trail(set_true_first_trail(*this, v));
         bool_var_data & d = m_bdata[v];
         d.set_true_first_flag();
     }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index cd1add643..16d6f41cc 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -110,9 +110,9 @@ namespace smt {
 
         unsigned                    m_final_check_idx; // circular counter used for implementing fairness
 
-        bool                        m_is_auxiliary; // used to prevent unwanted information from being logged.
-        class parallel*             m_par;
-        unsigned                    m_par_index;
+        bool                        m_is_auxiliary { false }; // used to prevent unwanted information from being logged.
+        class parallel*             m_par { nullptr };
+        unsigned                    m_par_index { 0 };
 
         // -----------------------------------
         //
@@ -151,7 +151,7 @@ namespace smt {
         svector<new_th_eq>          m_propagated_th_diseqs;
         svector<enode_pair>         m_diseq_vector;
 #endif
-        enode *                     m_is_diseq_tmp; // auxiliary enode used to find congruent equality atoms.
+        enode *                     m_is_diseq_tmp { nullptr }; // auxiliary enode used to find congruent equality atoms.
 
         tmp_enode                   m_tmp_enode;
         ptr_vector<almost_cg_table> m_almost_cg_tables; // temporary field for is_ext_diseq
@@ -180,15 +180,15 @@ namespace smt {
         literal_vector              m_assigned_literals;
         typedef std::pair<clause*, literal_vector> tmp_clause;
         vector<tmp_clause>          m_tmp_clauses;
-        unsigned                    m_qhead;
-        unsigned                    m_simp_qhead;
-        int                         m_simp_counter; //!< can become negative
+        unsigned                    m_qhead { 0 };
+        unsigned                    m_simp_qhead { 0 };
+        int                         m_simp_counter { 0 }; //!< can become negative
         scoped_ptr<case_split_queue> m_case_split_queue;
         scoped_ptr<induction>       m_induction;
-        double                      m_bvar_inc;
-        bool                        m_phase_cache_on;
-        unsigned                    m_phase_counter; //!< auxiliary variable used to decide when to turn on/off phase caching
-        bool                        m_phase_default; //!< default phase when using phase caching
+        double                      m_bvar_inc { 1.0 };
+        bool                        m_phase_cache_on { true };
+        unsigned                    m_phase_counter { 0 }; //!< auxiliary variable used to decide when to turn on/off phase caching
+        bool                        m_phase_default { false }; //!< default phase when using phase caching
 
         // A conflict is usually a single justification. That is, a justification
         // for false. If m_not_l is not null_literal, then m_conflict is a
@@ -600,10 +600,10 @@ namespace smt {
         //
         // -----------------------------------
     protected:
-        typedef ptr_vector<trail<context> >   trail_stack;
+        typedef ptr_vector<trail >   trail_stack;
         trail_stack                           m_trail_stack;
 #ifdef Z3DEBUG
-        bool                                  m_trail_enabled;
+        bool                                  m_trail_enabled { true };
 #endif
 
     public:
@@ -613,15 +613,15 @@ namespace smt {
             m_trail_stack.push_back(new (m_region) TrailObject(obj));
         }
 
-        void push_trail_ptr(trail<context> * ptr) {
+        void push_trail_ptr(trail * ptr) {
             m_trail_stack.push_back(ptr);
         }
 
     protected:
 
-        unsigned                    m_scope_lvl;
-        unsigned                    m_base_lvl;
-        unsigned                    m_search_lvl; // It is greater than m_base_lvl when assumptions are used.  Otherwise, it is equals to m_base_lvl
+        unsigned                    m_scope_lvl { 0 };
+        unsigned                    m_base_lvl { 0 };
+        unsigned                    m_search_lvl { 0 }; // It is greater than m_base_lvl when assumptions are used.  Otherwise, it is equals to m_base_lvl
         struct scope {
             unsigned                m_assigned_literals_lim;
             unsigned                m_trail_stack_lim;
@@ -724,7 +724,7 @@ namespace smt {
         }
 
     protected:
-        unsigned m_generation; //!< temporary variable used during internalization
+        unsigned m_generation { 0 }; //!< temporary variable used during internalization
 
     public:
         bool binary_clause_opt_enabled() const {
@@ -793,25 +793,31 @@ namespace smt {
         void internalize_uninterpreted(app * n);
 
         friend class mk_bool_var_trail;
-        class mk_bool_var_trail : public trail<context> {
+        class mk_bool_var_trail : public trail {
+            context& ctx;
         public:
-            void undo(context & ctx) override { ctx.undo_mk_bool_var(); }
+            mk_bool_var_trail(context& ctx) :ctx(ctx) {}
+            void undo() override { ctx.undo_mk_bool_var(); }
         };
         mk_bool_var_trail   m_mk_bool_var_trail;
         void undo_mk_bool_var();
 
         friend class mk_enode_trail;
-        class mk_enode_trail : public trail<context> {
+        class mk_enode_trail : public trail {
+            context& ctx;
         public:
-            void undo(context & ctx) override { ctx.undo_mk_enode(); }
+            mk_enode_trail(context& ctx) :ctx(ctx) {}
+            void undo() override { ctx.undo_mk_enode(); }
         };
         mk_enode_trail   m_mk_enode_trail;
         void undo_mk_enode();
 
         friend class mk_lambda_trail;
-        class mk_lambda_trail : public trail<context> {
+        class mk_lambda_trail : public trail {
+            context& ctx;
         public:
-            void undo(context & ctx) override { ctx.undo_mk_lambda(); }
+            mk_lambda_trail(context& ctx) :ctx(ctx) {}
+            void undo() override { ctx.undo_mk_lambda(); }
         };
         mk_lambda_trail   m_mk_lambda_trail;
         void undo_mk_lambda();
@@ -970,10 +976,10 @@ namespace smt {
         //
         // -----------------------------------
     protected:
-        lbool              m_last_search_result;
-        failure            m_last_search_failure;
+        lbool              m_last_search_result { l_undef };
+        failure            m_last_search_failure { UNKNOWN };
         ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model
-        bool               m_searching;
+        bool               m_searching { false };
         unsigned           m_num_conflicts;
         unsigned           m_num_conflicts_since_restart;
         unsigned           m_num_conflicts_since_lemma_gc;
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index a5d84feae..7eeab6388 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -137,7 +137,7 @@ namespace smt {
     void enode::set_generation(context & ctx, unsigned generation) {
         if (m_generation == generation)
             return;
-        ctx.push_trail(value_trail<context, unsigned>(m_generation));
+        ctx.push_trail(value_trail<unsigned>(m_generation));
         m_generation = generation;
     }
 
@@ -147,13 +147,13 @@ namespace smt {
         // m_lbl_hash should be different from -1, if and only if,
         // there is a pattern that contains the enode. So,
         // I use a trail to restore the value of m_lbl_hash to -1.
-        ctx.push_trail(value_trail<context, signed char>(m_lbl_hash));
+        ctx.push_trail(value_trail<signed char>(m_lbl_hash));
         unsigned h = hash_u(get_owner_id());
         m_lbl_hash = h & (APPROX_SET_CAPACITY - 1);
         // propagate modification to the root m_lbls set.
         approx_set & r_lbls = m_root->m_lbls;
         if (!r_lbls.may_contain(m_lbl_hash)) {
-            ctx.push_trail(value_trail<context, approx_set>(r_lbls));
+            ctx.push_trail(value_trail<approx_set>(r_lbls));
             r_lbls.insert(m_lbl_hash);
         }
     }
diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp
index 6f13a78b9..d5375b87e 100644
--- a/src/smt/smt_induction.cpp
+++ b/src/smt/smt_induction.cpp
@@ -58,7 +58,7 @@ literal_vector collect_induction_literals::pre_select() {
     }
     TRACE("induction", ctx.display(tout << "literal index: " << m_literal_index << "\n" << result << "\n"););
 
-    ctx.push_trail(value_trail<context, unsigned>(m_literal_index));
+    ctx.push_trail(value_trail<unsigned>(m_literal_index));
     m_literal_index = ctx.assigned_literals().size();
     return result;
 }
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 0e1aeef78..a08b58473 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -701,13 +701,13 @@ namespace smt {
     /**
        \brief Trail object to disable the m_merge_tf flag of an enode.
     */
-    class set_merge_tf_trail : public trail<context> {
+    class set_merge_tf_trail : public trail {
         enode * m_node;
     public:
         set_merge_tf_trail(enode * n):
             m_node(n) {
         }
-        void undo(context & ctx) override {
+        void undo() override {
             m_node->m_merge_tf = false;
         }
     };
@@ -747,13 +747,15 @@ namespace smt {
        variable. The flag m_enode is true for a Boolean variable v,
        if there is an enode n associated with it.
     */
-    class set_enode_flag_trail : public trail<context> {
+    class set_enode_flag_trail : public trail {
+        context& ctx;
         bool_var m_var;
     public:
-        set_enode_flag_trail(bool_var v):
+        set_enode_flag_trail(context& ctx, bool_var v):
+            ctx(ctx),
             m_var(v) {
         }
-        void undo(context & ctx) override {
+        void undo() override {
             bool_var_data & data = ctx.m_bdata[m_var];
             data.reset_enode_flag();
         }
@@ -770,7 +772,7 @@ namespace smt {
         bool_var_data & data = m_bdata[v];
         if (!data.is_enode()) {
             if (!is_new_var)
-                push_trail(set_enode_flag_trail(v));
+                push_trail(set_enode_flag_trail(*this, v));
             data.set_enode_flag();
         }
     }
@@ -1681,7 +1683,7 @@ namespace smt {
     /**
        \brief Trail for add_th_var
     */
-    class add_th_var_trail : public trail<context> {
+    class add_th_var_trail : public trail {
         enode *    m_enode;
         theory_id  m_th_id;
 #ifdef Z3DEBUG
@@ -1695,7 +1697,7 @@ namespace smt {
             SASSERT(m_th_var != null_theory_var);
         }
         
-        void undo(context & ctx) override {
+        void undo() override {
             theory_var v = m_enode->get_th_var(m_th_id);
             SASSERT(v != null_theory_var);
             SASSERT(m_th_var == v);
@@ -1709,7 +1711,7 @@ namespace smt {
     /**
        \brief Trail for replace_th_var
     */
-    class replace_th_var_trail : public trail<context> {
+    class replace_th_var_trail : public trail {
         enode *    m_enode;
         unsigned   m_th_id:8;
         unsigned   m_old_th_var:24;
@@ -1720,7 +1722,7 @@ namespace smt {
             m_old_th_var(old_var) {
         }
         
-        void undo(context & ctx) override {
+        void undo() override {
             SASSERT(m_enode->get_th_var(m_th_id) != null_theory_var);
             m_enode->replace_th_var(m_old_th_var, m_th_id);
         }
@@ -1762,7 +1764,7 @@ namespace smt {
             SASSERT(th->get_enode(old_v) != n); // this varialbe is not owned by n
             SASSERT(n->get_root()->get_th_var(th_id) != null_theory_var); // the root has also a variable in its var-list.
             n->replace_th_var(v, th_id);
-            push_trail(replace_th_var_trail(n, th_id, old_v));
+            push_trail(replace_th_var_trail( n, th_id, old_v));
             push_new_th_eq(th_id, v, old_v);
         }
         SASSERT(th->is_attached_to_var(n));
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 774906d05..b59e34454 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -754,7 +754,7 @@ namespace smt {
                 ptr_vector<enode>::const_iterator end = m_context->end_enodes();
                 unsigned sz = static_cast<unsigned>(end - it);
                 if (sz > m_new_enode_qhead) {
-                    m_context->push_trail(value_trail<context, unsigned>(m_new_enode_qhead));
+                    m_context->push_trail(value_trail<unsigned>(m_new_enode_qhead));
                     it += m_new_enode_qhead;
                     while (m_new_enode_qhead < sz) {
                         enode * e = *it;
@@ -799,7 +799,7 @@ namespace smt {
             if (use_ematching()) {
                 if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) {
                     m_lazy_mam->rematch();
-                    m_context->push_trail(value_trail<context, unsigned>(m_lazy_matching_idx));
+                    m_context->push_trail(value_trail<unsigned>(m_lazy_matching_idx));
                     m_lazy_matching_idx++;
                 }
             }
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index d25331a6d..1e52e0cbc 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -2228,7 +2228,7 @@ namespace smt {
         }
 
         if (result)
-            ctx.push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
+            ctx.push_trail(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
         return delayed_assume_eqs();
     }
 
@@ -2237,7 +2237,7 @@ namespace smt {
         if (m_assume_eq_head == m_assume_eq_candidates.size())
             return false;
 
-        ctx.push_trail(value_trail<context, unsigned>(m_assume_eq_head));
+        ctx.push_trail(value_trail<unsigned>(m_assume_eq_head));
         while (m_assume_eq_head < m_assume_eq_candidates.size()) {
             std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
             theory_var v1 = p.first;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 690e82786..d8bb38d55 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -31,7 +31,7 @@ namespace smt {
     void theory_arith<Ext>::found_unsupported_op(app * n) {
         if (!m_found_unsupported_op) {
             TRACE("arith", tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";);
-            ctx.push_trail(value_trail<context, bool>(m_found_unsupported_op));
+            ctx.push_trail(value_trail<bool>(m_found_unsupported_op));
             m_found_unsupported_op = true;
         }
     }
@@ -39,10 +39,10 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::found_underspecified_op(app * n) {
         m_underspecified_ops.push_back(n);
-        ctx.push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
+        ctx.push_trail(push_back_vector<ptr_vector<app>>(m_underspecified_ops));
         if (!m_found_underspecified_op) {
             TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, m) << "\n";);
-            ctx.push_trail(value_trail<context, bool>(m_found_underspecified_op));
+            ctx.push_trail(value_trail<bool>(m_found_underspecified_op));
             m_found_underspecified_op = true;
         }
 
@@ -1492,7 +1492,7 @@ namespace smt {
             return FC_CONTINUE;
         if (delayed_assume_eqs())
             return FC_CONTINUE;
-        ctx.push_trail(value_trail<context, unsigned>(m_final_check_idx));
+        ctx.push_trail(value_trail<unsigned>(m_final_check_idx));
         m_liberal_final_check = true;
         m_changed_assignment  = false;
         final_check_status result = final_check_core();
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 88e311f47..243bcc2c4 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -2138,7 +2138,7 @@ void theory_arith<Ext>::update_statistics(grobner & gb) {
 template<typename Ext>
 void theory_arith<Ext>::set_gb_exhausted() {
     IF_VERBOSE(3, verbose_stream() << "Grobner basis computation interrupted. Increase threshold using NL_ARITH_GB_THRESHOLD=<limit>\n";);
-    ctx.push_trail(value_trail<context, bool>(m_nl_gb_exhausted));
+    ctx.push_trail(value_trail<bool>(m_nl_gb_exhausted));
     m_nl_gb_exhausted = true;
 }
 
@@ -2314,7 +2314,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
         return FC_GIVEUP;
     }
 
-    ctx.push_trail(value_trail<context, unsigned>(m_nl_rounds));
+    ctx.push_trail(value_trail<unsigned>(m_nl_rounds));
     m_nl_rounds++;
 
     elim_quasi_base_rows();
@@ -2338,7 +2338,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
 
     bool progress;
     unsigned old_idx = m_nl_strategy_idx;
-    ctx.push_trail(value_trail<context, unsigned>(m_nl_strategy_idx));
+    ctx.push_trail(value_trail<unsigned>(m_nl_strategy_idx));
 
     do {
         progress = false;
diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index e0702f530..9a17f6e6a 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -90,7 +90,7 @@ namespace smt {
         var_data * d     = m_var_data[v];
         d->m_parent_selects.push_back(s);
         TRACE("array", tout << v << " " << mk_pp(s->get_owner(), m) << " " << mk_pp(get_enode(v)->get_owner(), m) << "\n";);
-        m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_selects));
+        m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_selects));
         for (enode* n : d->m_stores) {
             instantiate_axiom2a(s, n);
         }
@@ -111,7 +111,7 @@ namespace smt {
         v                = find(v);
         var_data * d     = m_var_data[v];
         d->m_parent_stores.push_back(s);
-        m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores));
+        m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_stores));
         if (d->m_prop_upward && !m_params.m_array_delay_exp_axiom) {
             for (enode* n : d->m_parent_selects) {
                 if (!m_params.m_array_cg || n->is_cgr()) {
@@ -143,7 +143,7 @@ namespace smt {
                 return;
             }
             TRACE("array", tout << "#" << v << "\n";);
-            m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
+            m_trail_stack.push(reset_flag_trail(d->m_prop_upward));
             d->m_prop_upward = true;
             if (!m_params.m_array_delay_exp_axiom) 
                 instantiate_axiom2b_for(v);
@@ -186,7 +186,7 @@ namespace smt {
             set_prop_upward(v, d);
         }
         d->m_stores.push_back(s);
-        m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_stores));
+        m_trail_stack.push(push_back_trail<enode *, false>(d->m_stores));
         for (enode * n : d->m_parent_selects) {
             SASSERT(is_select(n));
             instantiate_axiom2a(n, s);
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index 1a11c2fd6..13867364d 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -278,8 +278,8 @@ namespace smt {
             if (tns == sz2) {
                 std::cout << "SEEN " << smt << "\n";                
             }
-            ctx().push_trail(value_trail<context, bool>(i1.m_is_leaf, false));
-            ctx().push_trail(value_trail<context, bool>(i2.m_is_leaf, false));
+            ctx().push_trail(value_trail<bool>(i1.m_is_leaf, false));
+            ctx().push_trail(value_trail<bool>(i2.m_is_leaf, false));
             expr_ref k1(m), k2(m), k3(m);
             expr_ref sz_tms(m), sz_tns(m), sz_smt(m);
             k1 = m_autil.mk_card(tms);
@@ -332,7 +332,7 @@ namespace smt {
                     }  
                     literal lit = mk_eq(sz, m_arith.mk_int(value));
                     if (lit != true_literal && is_true(lit)) {
-                        ctx().push_trail(value_trail<context, rational>(i.m_size, value));
+                        ctx().push_trail(value_trail<rational>(i.m_size, value));
                         continue;
                     }
                     ctx().set_true_first_flag(lit.var());
@@ -442,14 +442,14 @@ namespace smt {
             return l_true;
         }
 
-        class remove_sz : public trail<context> {
+        class remove_sz : public trail {
             ast_manager& m;
             obj_map<app, sz_info*> & m_table;
             app*                     m_obj;
         public:
             remove_sz(ast_manager& m, obj_map<app, sz_info*>& tab, app* t): m(m), m_table(tab), m_obj(t) { }
             ~remove_sz() override {}
-            void undo(context& ctx) override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
+            void undo() override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
         };
 
         std::ostream& display(std::ostream& out) {
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index e65c383b6..683e0aa51 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -34,14 +34,14 @@ namespace smt {
     }
 
     void theory_array_base::add_weak_var(theory_var v) {
-        ctx.push_trail(push_back_vector<context, svector<theory_var>>(m_array_weak_trail));
+        ctx.push_trail(push_back_vector<svector<theory_var>>(m_array_weak_trail));
         m_array_weak_trail.push_back(v);
     }
 
     void theory_array_base::found_unsupported_op(expr * n) {
         if (!ctx.get_fparams().m_array_fake_support && !m_found_unsupported_op) {
             TRACE("array", tout << mk_ll_pp(n, m) << "\n";);            
-            ctx.push_trail(value_trail<context, bool>(m_found_unsupported_op));
+            ctx.push_trail(value_trail<bool>(m_found_unsupported_op));
             m_found_unsupported_op = true;
         }
     }
@@ -430,7 +430,7 @@ namespace smt {
             m_extensionality_todo.reset();
             m_congruent_todo.reset();
             if (!ctx.get_fparams().m_array_weak && has_propagate_up_trail()) {
-                ctx.push_trail(value_trail<context, unsigned>(m_array_weak_head));
+                ctx.push_trail(value_trail<unsigned>(m_array_weak_head));
                 for (; m_array_weak_head < m_array_weak_trail.size(); ++m_array_weak_head) {
                     set_prop_upward(m_array_weak_trail[m_array_weak_head]);
                 }                
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 782d8e6f6..a4772c578 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -54,7 +54,7 @@ namespace smt {
         //       instead apply stratified filter.
         set_prop_upward(v,d);
         d_full->m_maps.push_back(s);
-        m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_maps));
+        m_trail_stack.push(push_back_trail<enode *, false>(d_full->m_maps));
         for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
             enode* n = d->m_parent_selects[i];
             SASSERT(is_select(n));
@@ -88,7 +88,7 @@ namespace smt {
         var_data * d     = m_var_data[v];
         var_data_full * d_full     = m_var_data_full[v];
         d_full->m_parent_maps.push_back(s);
-        m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps));
+        m_trail_stack.push(push_back_trail<enode *, false>(d_full->m_parent_maps));
         if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
             for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
                 enode * n = d->m_parent_selects[i];
@@ -110,7 +110,7 @@ namespace smt {
                 add_weak_var(v);
                 return;
             }
-            m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
+            m_trail_stack.push(reset_flag_trail(d->m_prop_upward));
             d->m_prop_upward = true;
             TRACE("array", tout << "#" << v << "\n";);
             if (!m_params.m_array_delay_exp_axiom) {
@@ -171,7 +171,7 @@ namespace smt {
             set_prop_upward(v, d);
         }
         ptr_vector<enode> & consts = m_var_data_full[v]->m_consts;
-        m_trail_stack.push(push_back_trail<theory_array, enode *, false>(consts));
+        m_trail_stack.push(push_back_trail<enode *, false>(consts));
         consts.push_back(cnst);
         instantiate_default_const_axiom(cnst);
         for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
@@ -188,7 +188,7 @@ namespace smt {
             set_prop_upward(v, d);
         }
         ptr_vector<enode> & as_arrays = m_var_data_full[v]->m_as_arrays;
-        m_trail_stack.push(push_back_trail<theory_array, enode *, false>(as_arrays));
+        m_trail_stack.push(push_back_trail<enode *, false>(as_arrays));
         as_arrays.push_back(arr);
         instantiate_default_as_array_axiom(arr);        
         for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
@@ -744,11 +744,11 @@ namespace smt {
         func_decl* diag = nullptr;
         if (!m_sort2epsilon.find(s, eps)) {
             eps = m.mk_fresh_const("epsilon", s);
-            m_trail_stack.push(ast2ast_trail<theory_array, sort, app>(m_sort2epsilon, s, eps));   
+            m_trail_stack.push(ast2ast_trail<sort, app>(m_sort2epsilon, s, eps));   
         }
         if (!m_sort2diag.find(s, diag)) {
             diag = m.mk_fresh_func_decl("diag", 1, &s, s);
-            m_trail_stack.push(ast2ast_trail<theory_array, sort, func_decl>(m_sort2diag, s, diag));   
+            m_trail_stack.push(ast2ast_trail<sort, func_decl>(m_sort2diag, s, diag));   
         }
         return std::make_pair(eps, diag);
     }
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index b66fe36b7..19cdd7034 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -72,11 +72,12 @@ namespace smt {
 
     }
 
-    class mk_atom_trail : public trail<theory_bv> {
+    class mk_atom_trail : public trail {
+        theory_bv& th;
         bool_var m_var;
     public:
-        mk_atom_trail(bool_var v):m_var(v) {}
-        void undo(theory_bv & th) override {
+        mk_atom_trail(theory_bv& th, bool_var v):th(th), m_var(v) {}
+        void undo() override {
             theory_bv::atom * a = th.get_bv2a(m_var);
             a->~atom();
             th.erase_bv2a(m_var);
@@ -123,7 +124,7 @@ namespace smt {
             ctx.set_var_theory(bv, get_id());
             bit_atom * a     = new (get_region()) bit_atom();
             insert_bv2a(bv, a);
-            m_trail_stack.push(mk_atom_trail(bv));
+            m_trail_stack.push(mk_atom_trail(*this, bv));
             unsigned idx     = n->get_decl()->get_parameter(0).get_int();
             SASSERT(a->m_occs == 0);
             a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
@@ -212,11 +213,11 @@ namespace smt {
         get_bits(ctx.get_enode(arg), r);
     }
     
-    class add_var_pos_trail : public trail<theory_bv> {
+    class add_var_pos_trail : public trail {
         theory_bv::bit_atom * m_atom;
     public:
         add_var_pos_trail(theory_bv::bit_atom * a):m_atom(a) {}
-        void undo(theory_bv & th) override {
+        void undo() override {
             SASSERT(m_atom->m_occs);
             m_atom->m_occs = m_atom->m_occs->m_next;
         }
@@ -226,7 +227,7 @@ namespace smt {
         if (!params().m_bv_eq_axioms)
             return;
         m_prop_diseqs.push_back(bv_diseq(v1, v2, idx));
-        ctx.push_trail(push_back_vector<context, svector<bv_diseq>>(m_prop_diseqs));
+        ctx.push_trail(push_back_vector<svector<bv_diseq>>(m_prop_diseqs));
     }
 
     /**
@@ -302,7 +303,7 @@ namespace smt {
                 SASSERT(ctx.get_var_theory(l.var()) == get_id());
                 bit_atom * b = new (get_region()) bit_atom();
                 insert_bv2a(l.var(), b);
-                m_trail_stack.push(mk_atom_trail(l.var()));
+                m_trail_stack.push(mk_atom_trail(*this, l.var()));
                 SASSERT(b->m_occs == 0);
                 b->m_occs = new (get_region()) var_pos_occ(v, idx);
             }
@@ -947,7 +948,7 @@ namespace smt {
         ctx.set_var_theory(l.var(), get_id());                                                                  \
         le_atom * a     = new (get_region()) le_atom(l, def); /* abuse le_atom */                               \
         insert_bv2a(l.var(), a);                                                                                \
-        m_trail_stack.push(mk_atom_trail(l.var()));                                                             \
+        m_trail_stack.push(mk_atom_trail(*this, l.var()));                                                             \
         /* smul_no_overflow and umul_no_overflow are using the le_atom (THIS IS A BIG HACK)... */               \
         /* the connection between the l and def was never realized when                        */               \
         /* relevancy() is true and m_bv_lazy_le is false (the default configuration).          */               \
@@ -983,7 +984,7 @@ namespace smt {
         ctx.set_var_theory(l.var(), get_id());
         le_atom * a     = new (get_region()) le_atom(l, def);
         insert_bv2a(l.var(), a);
-        m_trail_stack.push(mk_atom_trail(l.var()));
+        m_trail_stack.push(mk_atom_trail(*this, l.var()));
         if (!ctx.relevancy() || !params().m_bv_lazy_le) {
             ctx.mk_th_axiom(get_id(),  l, ~def);
             ctx.mk_th_axiom(get_id(), ~l,  def);
@@ -1090,7 +1091,7 @@ namespace smt {
             if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) {                
                 if (!m_approximates_large_bvs) {
                     TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, m) << "\n";);
-                    ctx.push_trail(value_trail<context, bool>(m_approximates_large_bvs));
+                    ctx.push_trail(value_trail<bool>(m_approximates_large_bvs));
                     m_approximates_large_bvs = true;
                 }
                 return true;
@@ -1577,7 +1578,7 @@ namespace smt {
     void theory_bv::propagate() {
         if (!can_propagate())
             return;
-        ctx.push_trail(value_trail<context, unsigned>(m_prop_diseqs_qhead));
+        ctx.push_trail(value_trail<unsigned>(m_prop_diseqs_qhead));
         for (; m_prop_diseqs_qhead < m_prop_diseqs.size() && !ctx.inconsistent(); ++m_prop_diseqs_qhead) {
             auto p = m_prop_diseqs[m_prop_diseqs_qhead];
             assert_new_diseq_axiom(p.v1, p.v2, p.idx);
diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index 3faa5f73e..9d2fa598f 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -30,7 +30,7 @@ namespace smt {
         m_bits2char = symbol("bits2char");
     }
 
-    struct theory_char::reset_bits : public trail<context> {
+    struct theory_char::reset_bits : public trail {
         theory_char& s;
         unsigned idx;
 
@@ -39,7 +39,7 @@ namespace smt {
             idx(idx)
         {}
 
-        void undo(context& ctx) override {
+        void undo() override {
             s.m_bits[idx].reset();
             s.m_ebits[idx].reset();
         }
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index a7c8a26cc..e8169e21b 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -794,7 +794,7 @@ namespace smt {
                 ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, 1, &p)));
             }
             if (d1->m_constructor == nullptr) {
-                m_trail_stack.push(set_ptr_trail<theory_datatype, enode>(d1->m_constructor)); 
+                m_trail_stack.push(set_ptr_trail<enode>(d1->m_constructor)); 
                 // check whether there is a recognizer in d1 that conflicts with d2->m_constructor;
                 if (!d1->m_recognizers.empty()) {
                     unsigned c_idx = m_util.get_constructor_idx(d2->m_constructor->get_decl());
@@ -847,7 +847,7 @@ namespace smt {
             }
             SASSERT(val == l_undef || (val == l_false && d->m_constructor == 0));
             d->m_recognizers[c_idx] = recognizer;
-            m_trail_stack.push(set_vector_idx_trail<theory_datatype, enode>(d->m_recognizers, c_idx));
+            m_trail_stack.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
             if (val == l_false) {
                 propagate_recognizer(v, recognizer);
             }
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index d41bab49f..5baf6ccc1 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -124,7 +124,7 @@ namespace smt {
     void theory_dense_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
         if (!m_non_diff_logic_exprs) {
             TRACE("non_diff_logic", tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";);
-            ctx.push_trail(value_trail<context, bool>(m_non_diff_logic_exprs));
+            ctx.push_trail(value_trail<bool>(m_non_diff_logic_exprs));
             IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";); 
             m_non_diff_logic_exprs = true;
         }
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 544d69960..54c3188b0 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -171,7 +171,7 @@ void theory_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
     if (!m_non_diff_logic_exprs) {
         TRACE("non_diff_logic", tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";);
         IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";); 
-        ctx.push_trail(value_trail<context, bool>(m_non_diff_logic_exprs));
+        ctx.push_trail(value_trail<bool>(m_non_diff_logic_exprs));
         m_non_diff_logic_exprs = true;
     }
 }
@@ -557,7 +557,7 @@ void theory_diff_logic<Ext>::propagate() {
 
 template<typename Ext>
 void theory_diff_logic<Ext>::inc_conflicts() {
-    ctx.push_trail(value_trail<context, bool>(m_consistent));
+    ctx.push_trail(value_trail<bool>(m_consistent));
     m_consistent = false;
     m_stats.m_num_conflicts++;   
     if (m_params.m_arith_adaptive) {
diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index 6dd84f95d..60e0b8c03 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -209,8 +209,8 @@ namespace smt {
                 m_vals.insert(s, v);
                 add_trail(r);
                 add_trail(v);
-                ctx.push_trail(insert_obj_map<context,sort,func_decl*>(m_reps, s));
-                ctx.push_trail(insert_obj_map<context,sort,func_decl*>(m_vals, s));
+                ctx.push_trail(insert_obj_map<sort,func_decl*>(m_reps, s));
+                ctx.push_trail(insert_obj_map<sort,func_decl*>(m_vals, s));
             }
         }
 
@@ -283,7 +283,7 @@ namespace smt {
 
         void add_trail(ast* a) {
             m_trail.push_back(a);
-            ctx.push_trail(push_back_vector<context,ast_ref_vector>(m_trail));
+            ctx.push_trail(push_back_vector<ast_ref_vector>(m_trail));
         }
                 
     };
diff --git a/src/smt/theory_dummy.cpp b/src/smt/theory_dummy.cpp
index 938237a90..097d7f1ad 100644
--- a/src/smt/theory_dummy.cpp
+++ b/src/smt/theory_dummy.cpp
@@ -24,7 +24,7 @@ namespace smt {
 
     void theory_dummy::found_theory_expr() {
         if (!m_theory_exprs) {
-            get_context().push_trail(value_trail<context, bool>(m_theory_exprs));
+            get_context().push_trail(value_trail<bool>(m_theory_exprs));
             m_theory_exprs = true;
         }
     }
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 38d06f532..75289ddf8 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -188,7 +188,7 @@ namespace smt {
             m_conversions.insert(e, res);
             m.inc_ref(e);
             m.inc_ref(res);
-            m_trail_stack.push(insert_ref2_map<theory_fpa, ast_manager, expr, expr>(m, m_conversions, e, res.get()));
+            m_trail_stack.push(insert_ref2_map<ast_manager, expr, expr>(m, m_conversions, e, res.get()));
         }
 
         return res;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f160e5e8a..4eeba4e9d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -298,7 +298,7 @@ class theory_lra::imp {
     }
 
     void found_unsupported(expr* n) {
-        ctx().push_trail(value_trail<context, expr*>(m_not_handled));
+        ctx().push_trail(value_trail<expr*>(m_not_handled));
         TRACE("arith", tout << "unsupported " << mk_pp(n, m) << "\n";);
         m_not_handled = n;    
     }
@@ -733,7 +733,7 @@ class theory_lra::imp {
 
     void updt_unassigned_bounds(theory_var v, int inc) {
         TRACE("arith", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";);
-        ctx().push_trail(vector_value_trail<smt::context, unsigned, false>(m_unassigned_bounds, v));
+        ctx().push_trail(vector_value_trail<unsigned, false>(m_unassigned_bounds, v));
         m_unassigned_bounds[v] += inc;            
     }
        
@@ -1422,7 +1422,7 @@ public:
     void init_variable_values() {
         m_model_is_initialized = false;
         if (m.inc() && m_solver.get() && th.get_num_vars() > 0) {   
-            ctx().push_trail(value_trail<smt::context, bool>(m_model_is_initialized));
+            ctx().push_trail(value_trail<bool>(m_model_is_initialized));
             m_model_is_initialized = lp().init_model();
             TRACE("arith", display(tout << "update variable values " << m_model_is_initialized << "\n"););            
         }
@@ -1507,7 +1507,7 @@ public:
         }
             
         if (num_candidates > 0) {
-            ctx().push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
+            ctx().push_trail(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
         }
 
         return delayed_assume_eqs();
@@ -1517,7 +1517,7 @@ public:
         if (m_assume_eq_head == m_assume_eq_candidates.size())
             return false;
             
-        ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head));
+        ctx().push_trail(value_trail<unsigned>(m_assume_eq_head));
         while (m_assume_eq_head < m_assume_eq_candidates.size()) {
             std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
             theory_var v1 = p.first;
@@ -2960,7 +2960,7 @@ public:
             if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
                 TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";);
                 m_history.push_back(vec[ti]);
-                ctx().push_trail(history_trail<context, constraint_bound>(vec, ti, m_history));
+                ctx().push_trail(history_trail<constraint_bound>(vec, ti, m_history));
                 b.first = ci;
                 b.second = v;
             }
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 7c83580ac..2c6474c6c 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1093,11 +1093,11 @@ namespace smt {
         return lits;
     }
 
-    class theory_pb::negate_ineq : public trail<context> {
+    class theory_pb::negate_ineq : public trail {
         ineq& c;
     public:
         negate_ineq(ineq& c): c(c) {}
-        void undo(context& ctx) override {
+        void undo() override {
             c.negate();
         }
     };
@@ -1111,9 +1111,9 @@ namespace smt {
     void theory_pb::assign_ineq(ineq& c, bool is_true) {
         m_mpz_trail.push_back(c.m_max_sum);
         m_mpz_trail.push_back(c.m_min_sum);
-        ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_max_sum, m_mpz_trail));
-        ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_min_sum, m_mpz_trail));
-        ctx.push_trail(value_trail<context, unsigned>(c.m_nfixed));
+        ctx.push_trail(scoped_value_trail<scoped_mpz, scoped_mpz_vector>(c.m_max_sum, m_mpz_trail));
+        ctx.push_trail(scoped_value_trail<scoped_mpz, scoped_mpz_vector>(c.m_min_sum, m_mpz_trail));
+        ctx.push_trail(value_trail<unsigned>(c.m_nfixed));
 
         SASSERT(c.is_ge());
         unsigned sz = c.size();
@@ -1437,13 +1437,13 @@ namespace smt {
         c.m_min_sum.reset();
     }
 
-    class theory_pb::unwatch_ge : public trail<context> {
+    class theory_pb::unwatch_ge : public trail {
         theory_pb& pb;
         ineq&      c;
     public:
         unwatch_ge(theory_pb& p, ineq& c): pb(p), c(c) {}
         
-        void undo(context& ctx) override {
+        void undo() override {
             for (unsigned i = 0; i < c.watch_size(); ++i) {
                 pb.unwatch_literal(c.lit(i), &c);
             }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index a13b0b440..6fb4b3128 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -476,7 +476,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
         return false;
     }
     
-    m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_fixed, e));
+    m_trail_stack.push(insert_obj_trail<expr>(m_fixed, e));
     m_fixed.insert(e);
 
     expr_ref seq(e, m), head(m), tail(m);
@@ -501,7 +501,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
         return false;
     add_axiom(~a, b);
     if (!ctx.at_base_level()) {
-        m_trail_stack.push(push_replay(alloc(replay_fixed_length, m, len_e)));
+        m_trail_stack.push(push_replay(*this, alloc(replay_fixed_length, m, len_e)));
     }
     return true;
 }
@@ -620,7 +620,7 @@ bool theory_seq::check_lts() {
         return false;
     }
     unsigned sz = m_lts.size();
-    m_trail_stack.push(value_trail<theory_seq, bool>(m_lts_checked));
+    m_trail_stack.push(value_trail<bool>(m_lts_checked));
     m_lts_checked = true;
     expr* a = nullptr, *b = nullptr, *c = nullptr, *d = nullptr;
     bool is_strict1, is_strict2;
@@ -941,7 +941,7 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
     for (expr* r : rs) {
         if (m_util.str.is_unit(r, u) && !m_is_digit.contains(u)) {
             m_is_digit.insert(u);
-            m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_is_digit, u));
+            m_trail_stack.push(insert_obj_trail<expr>(m_is_digit, u));
             literal is_digit = m_ax.is_digit(u);
             if (ctx.get_assignment(is_digit) != l_true) {
                 propagate_lit(dep, 0, nullptr, is_digit);
@@ -1508,8 +1508,8 @@ void theory_seq::add_length(expr* e, expr* l) {
     SASSERT(!m_has_length.contains(l));
     m_length.push_back(l);
     m_has_length.insert(e);
-    m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_has_length, e));
-    m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_length));
+    m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e));
+    m_trail_stack.push(push_back_vector<expr_ref_vector>(m_length));
 }
 
 /**
@@ -1529,11 +1529,11 @@ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
     }
     m_length_limit_map.insert(s, k);
     m_length_limit.push_back(lim_e);    
-    m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_length_limit));    
+    m_trail_stack.push(push_back_vector<expr_ref_vector>(m_length_limit));    
     if (k0 != 0) {
-        m_trail_stack.push(remove_obj_map<theory_seq, expr, unsigned>(m_length_limit_map, s, k0));
+        m_trail_stack.push(remove_obj_map<expr, unsigned>(m_length_limit_map, s, k0));
     }
-    m_trail_stack.push(insert_obj_map<theory_seq, expr, unsigned>(m_length_limit_map, s));
+    m_trail_stack.push(insert_obj_map<expr, unsigned>(m_length_limit_map, s));
     if (is_searching) {
         expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth);
         add_axiom(~mk_literal(dlimit), mk_literal(lim_e));
@@ -1564,7 +1564,7 @@ bool theory_seq::add_length_to_eqc(expr* e) {
 
 void theory_seq::add_int_string(expr* e) {
     m_int_string.push_back(e);
-    m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_int_string));
+    m_trail_stack.push(push_back_vector<expr_ref_vector>(m_int_string));
 }
 
 bool theory_seq::check_int_string() {
@@ -2514,8 +2514,8 @@ void theory_seq::enque_axiom(expr* e) {
         TRACE("seq", tout << "add axiom " << mk_bounded_pp(e, m) << "\n";);
         m_axioms.push_back(e);
         m_axiom_set.insert(e);
-        m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
-        m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_axiom_set, e));;
+        m_trail_stack.push(push_back_vector<expr_ref_vector>(m_axioms));
+        m_trail_stack.push(insert_obj_trail<expr>(m_axiom_set, e));;
     }
 }
 
@@ -2524,7 +2524,7 @@ void theory_seq::deque_axiom(expr* n) {
     if (m_util.str.is_length(n)) {
         m_ax.add_length_axiom(n);
         if (!ctx.at_base_level()) {
-            m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
+            m_trail_stack.push(push_replay(*this, alloc(replay_axiom, m, n)));
         }
     }
     else if (m_util.str.is_empty(n) && !has_length(n) && !m_has_length.empty()) {
@@ -3034,7 +3034,7 @@ void theory_seq::push_scope_eh() {
     m_exclude.push_scope();
     m_dm.push_scope();
     m_trail_stack.push_scope();
-    m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
+    m_trail_stack.push(value_trail<unsigned>(m_axioms_head));
     m_eqs.push_scope();
     m_nqs.push_scope();
     m_ncs.push_scope();
@@ -3108,7 +3108,7 @@ void theory_seq::relevant_eh(app* n) {
 
 void theory_seq::add_unhandled_expr(expr* n) {
     if (!m_unhandled_expr) {
-        ctx.push_trail(value_trail<context, expr*>(m_unhandled_expr));
+        ctx.push_trail(value_trail<expr*>(m_unhandled_expr));
         m_unhandled_expr = n;
     }
 }
@@ -3118,7 +3118,7 @@ void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
     if (m_has_seq) {
         TRACE("seq", tout << "add_theory_assumption\n";);
         expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth);
-        m_trail_stack.push(value_trail<theory_seq, literal>(m_max_unfolding_lit));
+        m_trail_stack.push(value_trail<literal>(m_max_unfolding_lit));
         m_max_unfolding_lit = mk_literal(dlimit);        
         assumptions.push_back(dlimit);
         for (auto const& kv : m_length_limit_map) {
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 563efd230..d9f73e541 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -281,20 +281,22 @@ namespace smt {
             }
         };
 
-        class push_replay : public trail<theory_seq> {
+        class push_replay : public trail {
+            theory_seq& th;
             apply* m_apply;
         public:
-            push_replay(apply* app): m_apply(app) {}
-            void undo(theory_seq& th) override {
+            push_replay(theory_seq& th, apply* app): th(th), m_apply(app) {}
+            void undo() override {
                 th.m_replay.push_back(m_apply);
             }
         };
 
-        class pop_branch : public trail<theory_seq> {
+        class pop_branch : public trail {
+            theory_seq& th;
             unsigned k;
         public:
-            pop_branch(unsigned k): k(k) {}
-            void undo(theory_seq& th) override {
+            pop_branch(theory_seq& th, unsigned k): th(th), k(k) {}
+            void undo() override {
                 th.m_branch_start.erase(k);
             }
         };
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index 590878daa..5562ba01b 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -28,7 +28,7 @@ namespace smt {
     class theory_seq_empty : public theory {
         bool m_used;
         final_check_status final_check_eh() override { return m_used?FC_GIVEUP:FC_DONE; }
-        bool internalize_atom(app*, bool) override { if (!m_used) { get_context().push_trail(value_trail<context,bool>(m_used)); m_used = true; } return false; }
+        bool internalize_atom(app*, bool) override { if (!m_used) { get_context().push_trail(value_trail<bool>(m_used)); m_used = true; } return false; }
         bool internalize_term(app*) override { return internalize_atom(nullptr,false);  }
         void new_eq_eh(theory_var, theory_var) override { }
         void new_diseq_eh(theory_var, theory_var) override {}
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 04b5c4608..d7f6f2757 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6827,12 +6827,12 @@ namespace smt {
                     m_concat_eval_todo.push_back(n);
                 } else if (u.str.is_at(ap) || u.str.is_extract(ap) || u.str.is_replace(ap)) {
                     m_library_aware_axiom_todo.push_back(n);
-                    m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
+                    m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
                 } else if (u.str.is_itos(ap)) {
                     TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
                     string_int_conversion_terms.push_back(ap);
                     m_library_aware_axiom_todo.push_back(n);
-                    m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
+                    m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
                 } else if (is_var(ex)) {
                     // if ex is a variable, add it to our list of variables
                     TRACE("str", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;);
@@ -6858,7 +6858,7 @@ namespace smt {
                     app * ap = to_app(ex);
                     if (u.str.is_prefix(ap) || u.str.is_suffix(ap) || u.str.is_contains(ap) || u.str.is_in_re(ap)) {
                         m_library_aware_axiom_todo.push_back(n);
-                        m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
+                        m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
                     }
                 }
             } else {
@@ -6878,12 +6878,12 @@ namespace smt {
                 app * ap = to_app(ex);
                 if (u.str.is_index(ap)) {
                     m_library_aware_axiom_todo.push_back(n);
-                    m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
+                    m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
                 } else if (u.str.is_stoi(ap)) {
                     TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
                     string_int_conversion_terms.push_back(ap);
                     m_library_aware_axiom_todo.push_back(n);
-                    m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
+                    m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
                 }
             }
         } else {
@@ -8151,7 +8151,7 @@ namespace smt {
                         if (!string_int_axioms.contains(axiom)) {
                             string_int_axioms.insert(axiom);
                             assert_axiom(axiom);
-                            m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
+                            m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
                             axiomAdd = true;
                         }
                     } else {
@@ -8185,7 +8185,7 @@ namespace smt {
                 if (!string_int_axioms.contains(axiom)) {
                     string_int_axioms.insert(axiom);
                     assert_axiom(axiom);
-                    m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
+                    m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
                     axiomAdd = true;
                 }
             } else {
@@ -8195,7 +8195,7 @@ namespace smt {
                 if (!string_int_axioms.contains(axiom)) {
                     string_int_axioms.insert(axiom);
                     assert_axiom(axiom);
-                    m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
+                    m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
                     axiomAdd = true;
                 }
             }
@@ -8239,7 +8239,7 @@ namespace smt {
                     if (!string_int_axioms.contains(axiom)) {
                         string_int_axioms.insert(axiom);
                         assert_axiom(axiom);
-                        m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
+                        m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
                         axiomAdd = true;
                     }
                 } else {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 24dde6b5d..f659402fb 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -86,14 +86,14 @@ public:
 class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
 
 template<typename Ctx>
-class binary_search_trail : public trail<Ctx> {
+class binary_search_trail : public trail {
     obj_map<expr, ptr_vector<expr> > & target;
     expr * entry;
 public:
     binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
         target(target), entry(entry) {}
     ~binary_search_trail() override {}
-    void undo(Ctx & ctx) override {
+    void undo() override {
         TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
         if (target.contains(entry)) {
             if (!target[entry].empty()) {
diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp
index ecdc0c14c..36e1f2117 100644
--- a/src/smt/theory_str_regex.cpp
+++ b/src/smt/theory_str_regex.cpp
@@ -107,7 +107,7 @@ namespace smt {
                     }
 
                     regex_terms_with_length_constraints.insert(str_in_re);
-                    m_trail_stack.push(insert_obj_trail<theory_str, expr>(regex_terms_with_length_constraints, str_in_re));
+                    m_trail_stack.push(insert_obj_trail<expr>(regex_terms_with_length_constraints, str_in_re));
                     regex_axiom_add = true;
                 }
             } // re not in regex_terms_with_length_constraints
@@ -179,7 +179,7 @@ namespace smt {
                             expr_ref rhs(ctx.mk_eq_atom(str, mk_string("")), m);
                             assert_implication(lhs, rhs);
                             regex_terms_with_path_constraints.insert(str_in_re);
-                            m_trail_stack.push(insert_obj_trail<theory_str, expr>(regex_terms_with_path_constraints, str_in_re));
+                            m_trail_stack.push(insert_obj_trail<expr>(regex_terms_with_path_constraints, str_in_re));
                         } else {
                             TRACE("str", tout << "zero-length solution not admitted by this automaton -- asserting conflict clause" << std::endl;);
                             expr_ref_vector lhs_terms(m);
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 954ad4a51..1188d8192 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -190,7 +190,7 @@ namespace smt {
 
     template<typename Ext>
     void theory_utvpi<Ext>::inc_conflicts() {
-        ctx.push_trail(value_trail<context, bool>(m_consistent));
+        ctx.push_trail(value_trail<bool>(m_consistent));
         m_consistent = false;
         m_stats.m_num_conflicts++;   
         if (m_params.m_arith_adaptive) {
@@ -238,7 +238,7 @@ namespace smt {
         auto str = msg.str();
         TRACE("utvpi", tout << str;);
         warning_msg("%s", str.c_str());
-        ctx.push_trail(value_trail<context, bool>(m_non_utvpi_exprs));
+        ctx.push_trail(value_trail<bool>(m_non_utvpi_exprs));
         m_non_utvpi_exprs = true;        
     }
 
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index 791d550a4..9113f76d6 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/src/smt/theory_wmaxsat.cpp
@@ -161,8 +161,8 @@ namespace smt {
             scoped_mpz w(m_mpz);
             w = m_zweights[tv];
             ctx.push_trail(numeral_trail(m_zcost, m_old_values));
-            ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
-            ctx.push_trail(value_trail<context, bool>(m_assigned[tv]));
+            ctx.push_trail(push_back_vector<svector<theory_var> >(m_costs));
+            ctx.push_trail(value_trail<bool>(m_assigned[tv]));
             m_zcost += w;
             TRACE("opt", tout << "Assign v" << tv << " weight: " << w << " cost: " << m_zcost << " " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << "\n";);
             m_costs.push_back(tv);
@@ -299,7 +299,7 @@ namespace smt {
         }
         // 
         if (max_unassigned > m_max_unassigned_index) {
-            ctx.push_trail(value_trail<context, unsigned>(m_max_unassigned_index));
+            ctx.push_trail(value_trail<unsigned>(m_max_unassigned_index));
             m_max_unassigned_index = max_unassigned;
         }
         if (max_unassigned < m_sorted_vars.size() && 
diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h
index 3a24dca10..236f56bee 100644
--- a/src/smt/theory_wmaxsat.h
+++ b/src/smt/theory_wmaxsat.h
@@ -64,7 +64,7 @@ namespace smt {
         rational get_cost();
         void init_min_cost(rational const& r);
 
-        class numeral_trail : public trail<context> {
+        class numeral_trail : public trail {
             typedef scoped_mpz T;
             T & m_value;
             scoped_mpz_vector&  m_old_values;            
@@ -78,7 +78,7 @@ namespace smt {
             ~numeral_trail() override {
             }
             
-            void undo(context & ctx) override {
+            void undo() override {
                 m_value = m_old_values.back();
                 m_old_values.shrink(m_old_values.size() - 1);
             }
diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp
index bfdcbb3ba..3fd58ff4d 100644
--- a/src/smt/user_propagator.cpp
+++ b/src/smt/user_propagator.cpp
@@ -84,7 +84,7 @@ void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits,
     if (m_fixed.contains(v))
         return;
     m_fixed.insert(v);
-    ctx.push_trail(insert_map<context, uint_set, unsigned>(m_fixed, v));
+    ctx.push_trail(insert_map<uint_set, unsigned>(m_fixed, v));
     m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector());
     m_fixed_eh(m_user_context, this, v, value);
 }
@@ -142,7 +142,7 @@ void user_propagator::propagate() {
         ++m_stats.m_num_propagations;
         ++qhead;
     }
-    ctx.push_trail(value_trail<context, unsigned>(m_qhead));
+    ctx.push_trail(value_trail<unsigned>(m_qhead));
     m_qhead = qhead;
 }
 
diff --git a/src/util/trail.h b/src/util/trail.h
index 031ccdef2..2f3e5ecde 100644
--- a/src/util/trail.h
+++ b/src/util/trail.h
@@ -23,16 +23,16 @@ Revision History:
 #include "util/obj_ref.h"
 #include "util/vector.h"
 
-template<typename Ctx>
+
 class trail {
 public:
     virtual ~trail() {
     }
-    virtual void undo(Ctx & ctx) = 0;
+    virtual void undo() = 0;
 };
 
-template<typename Ctx, typename T>
-class value_trail : public trail<Ctx> {
+template<typename T>
+class value_trail : public trail {
     T & m_value;
     T   m_old_value;
 
@@ -51,15 +51,15 @@ public:
     ~value_trail() override {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_value = m_old_value;
     }
 };
 
 
     
-template<typename Ctx, typename T, typename Ts>
-class scoped_value_trail : public trail<Ctx> {
+template<typename T, typename Ts>
+class scoped_value_trail : public trail {
     T & m_value;
     Ts & m_values;
     
@@ -72,15 +72,14 @@ public:
     ~scoped_value_trail() override {
     }
     
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_value = m_values.back();
         m_values.pop_back();
     }
 };
 
 
-template<typename Ctx>
-class reset_flag_trail : public trail<Ctx> {
+class reset_flag_trail : public trail {
     bool & m_value;
 public:
     reset_flag_trail(bool & value):
@@ -90,13 +89,13 @@ public:
     ~reset_flag_trail() override {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_value = false;
     }
 };
 
-template<typename Ctx, typename T>
-class set_ptr_trail : public trail<Ctx> {
+template<typename T>
+class set_ptr_trail : public trail {
     T * & m_ptr;
 public:
     set_ptr_trail(T * & ptr):
@@ -104,13 +103,13 @@ public:
         SASSERT(m_ptr == 0);
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_ptr = nullptr;
     }
 };
 
-template<typename Ctx, typename T, bool CallDestructors=true>
-class restore_size_trail : public trail<Ctx> {
+template<typename T, bool CallDestructors=true>
+class restore_size_trail : public trail {
     vector<T, CallDestructors> & m_vector;
     unsigned                     m_old_size;
 public:
@@ -124,13 +123,13 @@ public:
     }
     ~restore_size_trail() override {
     }
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_vector.shrink(m_old_size);
     }
 };
 
-template<typename Ctx, typename T, bool CallDestructors=true>
-class vector_value_trail : public trail<Ctx> {
+template<typename T, bool CallDestructors=true>
+class vector_value_trail : public trail {
     vector<T, CallDestructors> & m_vector;
     unsigned                     m_idx;
     T                            m_old_value;
@@ -144,13 +143,13 @@ public:
     ~vector_value_trail() override {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_vector[m_idx] = m_old_value;
     }
 };
 
-template<typename Ctx, typename V, typename T>
-class vector2_value_trail : public trail<Ctx> {
+template<typename V, typename T>
+class vector2_value_trail : public trail {
     V             & m_vector;
     unsigned        m_i;
     unsigned        m_j;
@@ -166,57 +165,57 @@ public:
     ~vector2_value_trail() override {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_vector[m_i][m_j] = m_old_value;
     }
 };
 
 
-template<typename Ctx, typename D, typename R>
-class insert_obj_map : public trail<Ctx> {
+template<typename D, typename R>
+class insert_obj_map : public trail {
     obj_map<D,R>&     m_map;
     D*                m_obj;
 public:
     insert_obj_map(obj_map<D,R>& t, D* o) : m_map(t), m_obj(o) {}
     ~insert_obj_map() override {}
-    void undo(Ctx & ctx) override { m_map.remove(m_obj); }
+    void undo() override { m_map.remove(m_obj); }
 };
 
-template<typename Ctx, typename D, typename R>
-class remove_obj_map : public trail<Ctx> {
+template<typename D, typename R>
+class remove_obj_map : public trail {
     obj_map<D,R>&     m_map;
     D*                m_obj;
     R                 m_value;
 public:
     remove_obj_map(obj_map<D,R>& t, D* o, R v) : m_map(t), m_obj(o), m_value(v) {}
     ~remove_obj_map() override {}
-    void undo(Ctx & ctx) override { m_map.insert(m_obj, m_value); }
+    void undo() override { m_map.insert(m_obj, m_value); }
 };
 
-template<typename Ctx, typename M, typename D>
-class insert_map : public trail<Ctx> {
+template<typename M, typename D>
+class insert_map : public trail {
     M&            m_map;
     D             m_obj;
 public:
     insert_map(M& t, D o) : m_map(t), m_obj(o) {}
     ~insert_map() override {}
-    void undo(Ctx & ctx) override { m_map.remove(m_obj); }
+    void undo() override { m_map.remove(m_obj); }
 };
 
 
-template<typename Ctx, typename M, typename Mgr, typename D>
-class insert_ref_map : public trail<Ctx> {
+template<typename M, typename Mgr, typename D>
+class insert_ref_map : public trail {
     Mgr&          m;
     M&            m_map;
     D             m_obj;
 public:
     insert_ref_map(Mgr& m, M& t, D o) : m(m), m_map(t), m_obj(o) {}
     virtual ~insert_ref_map() {}
-    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); }
+    virtual void undo() { m_map.remove(m_obj); m.dec_ref(m_obj); }
 };
 
-template<typename Ctx, typename Mgr, typename D, typename R>
-class insert_ref2_map : public trail<Ctx> {
+template<typename Mgr, typename D, typename R>
+class insert_ref2_map : public trail {
     Mgr&           m;
     obj_map<D,R*>&  m_map;
     D*             m_obj;
@@ -224,25 +223,25 @@ class insert_ref2_map : public trail<Ctx> {
 public:
     insert_ref2_map(Mgr& m, obj_map<D,R*>& t, D*o, R*r) : m(m), m_map(t), m_obj(o), m_val(r) {}
     virtual ~insert_ref2_map() {}
-    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
+    virtual void undo() { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
 };
 
 
-template<typename Ctx, typename V>
-class push_back_vector : public trail<Ctx> {
+template<typename V>
+class push_back_vector : public trail {
     V & m_vector;
 public:
     push_back_vector(V & v):
         m_vector(v) {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_vector.pop_back();
     }
 };
 
-template<typename Ctx, typename T>
-class set_vector_idx_trail : public trail<Ctx> {
+template<typename T>
+class set_vector_idx_trail : public trail {
     ptr_vector<T> & m_vector;
     unsigned                         m_idx;
 public:
@@ -254,13 +253,13 @@ public:
     ~set_vector_idx_trail() override {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_vector[m_idx] = 0;
     }
 };
 
-template<typename Ctx, typename T, bool CallDestructors=true>
-class pop_back_trail : public trail<Ctx> {
+template<typename T, bool CallDestructors=true>
+class pop_back_trail : public trail {
     vector<T, CallDestructors> & m_vector;
     T m_value;
 public:
@@ -269,13 +268,13 @@ public:
     m_value(m_vector.back()) {
     }
 
-    virtual void undo(Ctx & ctx) {
+    virtual void undo() {
         m_vector.push_back(m_value);
     }
 };
 
-template<typename Ctx, typename T, bool CallDestructors=true>
-class pop_back2_trail : public trail<Ctx> {
+template<typename T, bool CallDestructors=true>
+class pop_back2_trail : public trail {
     vector<T, CallDestructors> & m_vector;
     typedef vector<vector<T, CallDestructors>, true> vector_t;
     unsigned m_index;
@@ -287,28 +286,28 @@ public:
     m_value(m_vector[index].back()) {
     }
 
-    virtual void undo(Ctx & ctx) {
+    virtual void undo() {
         m_vector[m_index].push_back(m_value);
     }
 };
 
 
 
-template<typename Ctx, typename T, bool CallDestructors=true>
-class push_back_trail : public trail<Ctx> {
+template<typename T, bool CallDestructors=true>
+class push_back_trail : public trail {
     vector<T, CallDestructors> & m_vector;
 public:
     push_back_trail(vector<T, CallDestructors> & v):
         m_vector(v) {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_vector.pop_back();
     }
 };
 
-template<typename Ctx, typename T, bool CallDestructors=true>
-class push_back2_trail : public trail<Ctx> {
+template<typename T, bool CallDestructors=true>
+class push_back2_trail : public trail {
     typedef vector<vector<T, CallDestructors>, true> vector_t;
     vector_t & m_vector;
     unsigned   m_index;
@@ -318,13 +317,13 @@ public:
     m_index(index) {
     }
 
-    virtual void undo(Ctx & ctx) {
+    virtual void undo() {
         m_vector[m_index].pop_back();
     }
 };
 
-template<typename Ctx>
-class set_bitvector_trail : public trail<Ctx> {
+
+class set_bitvector_trail : public trail {
     bool_vector & m_vector;
     unsigned        m_idx;
 public:
@@ -335,14 +334,14 @@ public:
         m_vector[m_idx] = true;
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         m_vector[m_idx] = false;
     }
 };
 
 
-template<typename Ctx, typename T, bool CallDestructors = true>
-class history_trail : public trail<Ctx> {
+template<typename T, bool CallDestructors = true>
+class history_trail : public trail {
     vector<T, CallDestructors>& m_dst;
     unsigned                     m_idx;
     vector<T, CallDestructors>& m_hist;
@@ -355,69 +354,69 @@ public:
     ~history_trail() override {
     }
     
-    void undo(Ctx& ctx) override {
+    void undo() override {
         m_dst[m_idx] = m_hist.back();
         m_hist.pop_back();
     }
 };
 
 
-template<typename Ctx, typename T>
-class new_obj_trail : public trail<Ctx> {
+template<typename T>
+class new_obj_trail : public trail {
     T * m_obj;
 public:
     new_obj_trail(T * obj):
         m_obj(obj) {
     }
 
-    void undo(Ctx & ctx) override {
+    void undo() override {
         dealloc(m_obj);
     }
 };
 
-template<typename Ctx, typename M, typename T>
-class obj_ref_trail : public trail<Ctx> {
+template<typename M, typename T>
+class obj_ref_trail : public trail {
     obj_ref<T,M> m_obj;
 public:
     obj_ref_trail(obj_ref<T,M>& obj):
         m_obj(obj) {
     }
 
-    virtual void undo(Ctx & ctx) {
+    virtual void undo() {
         m_obj.reset();
     }
 };
 
-template<typename Ctx, typename T>
-class insert_obj_trail : public trail<Ctx> {
+template<typename T>
+class insert_obj_trail : public trail {
     obj_hashtable<T>& m_table;
     T*                m_obj;
 public:
     insert_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
     ~insert_obj_trail() override {}
-    void undo(Ctx & ctx) override { m_table.remove(m_obj); }
+    void undo() override { m_table.remove(m_obj); }
 };
 
 
-template<typename Ctx, typename T>
-class remove_obj_trail : public trail<Ctx> {
+template<typename T>
+class remove_obj_trail : public trail {
     obj_hashtable<T>& m_table;
     T*                m_obj;
 public:
     remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
     virtual ~remove_obj_trail() {}
-    virtual void undo(Ctx & ctx) { m_table.insert(m_obj); }
+    virtual void undo() { m_table.insert(m_obj); }
 };
 
 
 template<typename Ctx>
-void undo_trail_stack(Ctx & ctx, ptr_vector<trail<Ctx> > & s, unsigned old_size) {
+void undo_trail_stack(Ctx & ctx, ptr_vector<trail> & s, unsigned old_size) {
     SASSERT(old_size <= s.size());
-    typename ptr_vector<trail<Ctx> >::iterator begin = s.begin() + old_size;
-    typename ptr_vector<trail<Ctx> >::iterator it    = s.end();
+    typename ptr_vector<trail >::iterator begin = s.begin() + old_size;
+    typename ptr_vector<trail >::iterator it    = s.end();
     while (it != begin) {
         --it;
-        (*it)->undo(ctx);
+        (*it)->undo();
     }
     s.shrink(old_size);
 }
@@ -425,7 +424,7 @@ void undo_trail_stack(Ctx & ctx, ptr_vector<trail<Ctx> > & s, unsigned old_size)
 template<typename Ctx>
 class trail_stack {
     Ctx &                   m_ctx;
-    ptr_vector<trail<Ctx> > m_trail_stack;
+    ptr_vector<trail>       m_trail_stack;
     unsigned_vector         m_scopes;
     region                  m_region;
 public:
@@ -441,7 +440,7 @@ public:
         undo_trail_stack(m_ctx, m_trail_stack, 0);
     }
 
-    void push_ptr(trail<Ctx> * t) { m_trail_stack.push_back(t); }
+    void push_ptr(trail * t) { m_trail_stack.push_back(t); }
 
     template<typename TrailObject>
     void push(TrailObject const & obj) { m_trail_stack.push_back(new (m_region) TrailObject(obj)); }
diff --git a/src/util/union_find.h b/src/util/union_find.h
index f706cd162..e6ab80f8a 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -47,12 +47,12 @@ class union_find {
     class mk_var_trail;
     friend class mk_var_trail;
 
-    class mk_var_trail : public trail<StackCtx> {
+    class mk_var_trail : public trail {
         union_find & m_owner;
     public:
         mk_var_trail(union_find & o):m_owner(o) {}
         ~mk_var_trail() override {}
-        void undo(StackCtx& ctx) override {
+        void undo() override {
             m_owner.m_find.pop_back();
             m_owner.m_size.pop_back();
             m_owner.m_next.pop_back();
@@ -64,13 +64,13 @@ class union_find {
     class merge_trail;
     friend class merge_trail;
 
-    class merge_trail : public trail<StackCtx> {
+    class merge_trail : public trail {
         union_find & m_owner;
         unsigned     m_r1;
     public:
         merge_trail(union_find & o, unsigned r1):m_owner(o), m_r1(r1) {}
         ~merge_trail() override {}
-        void undo(StackCtx& ctx) override { m_owner.unmerge(m_r1); }
+        void undo() override { m_owner.unmerge(m_r1); }
     };
 
     void unmerge(unsigned r1) {