diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp
index dcf6a7c59..79cad2fb2 100644
--- a/src/ackermannization/ackermannize_bv_tactic.cpp
+++ b/src/ackermannization/ackermannize_bv_tactic.cpp
@@ -31,6 +31,8 @@ public:
 
     ~ackermannize_bv_tactic() override { }
 
+    char const* name() const override { return "ackermannize_bv"; }
+
     void operator()(goal_ref const & g, goal_ref_buffer & result) override {
         tactic_report report("ackermannize_bv", *g);
         fail_if_unsat_core_generation("ackermannize", g);
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index c453806bf..1bc0cb630 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -220,6 +220,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "subpaving"; }
+
     tactic * translate(ast_manager & m) override {
         return alloc(subpaving_tactic, m, m_params);
     }
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 591e57944..b66ddf275 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -392,6 +392,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "horn"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index 8de478199..ddf85ce19 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -223,6 +223,8 @@ public:
         SASSERT(m_imp == 0);
     }
 
+    char const* name() const override { return "nlsat"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
     }
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 6439a91c9..28cfa5c3e 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -839,6 +839,8 @@ namespace qe {
         ~nlqsat() override {
         }
 
+        char const* name() const override { return "nlqsat"; }
+
         void updt_params(params_ref const & p) override {
             params_ref p2(p);
             p2.set_bool("factor", false);
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 58fe3b293..f6dd9c712 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2459,6 +2459,8 @@ public:
         m_params(p),
         m_qe(m, p, true) {}
 
+    char const* name() const override { return "qe_lite"; }
+
     tactic * translate(ast_manager & m) override {
         return alloc(qe_lite_tactic, m, m_params);
     }
diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
index 0aa3824e7..da1ce5efd 100644
--- a/src/qe/qe_tactic.cpp
+++ b/src/qe/qe_tactic.cpp
@@ -100,6 +100,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "qe"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 537a7ab56..767b96e5d 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -1257,6 +1257,8 @@ namespace qe {
         ~qsat() override {
             clear();
         }
+
+        char const* name() const override { return "qsat"; }
         
         void updt_params(params_ref const & p) override {
         }
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 521a70fb7..38c25eae3 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -198,6 +198,8 @@ public:
         SASSERT(m_imp == 0);
     }
 
+    char const* name() const override { return "sat"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         if (m_imp) m_imp->updt_params(p);
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index fd05c4a8e..6b1d1b7f4 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -63,6 +63,8 @@ public:
         m_fns.reset();
     }
 
+    char const* name() const override { return "ctx_solver_simplify"; }
+
     void updt_params(params_ref const & p) override {
         m_solver.updt_params(p);
     }
diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index 9e9d3a9de..5cbe469fd 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -41,18 +41,16 @@ class smt_tactic : public tactic {
     smt_params                   m_params;
     params_ref                   m_params_ref;
     statistics                   m_stats;
-    smt::kernel *                m_ctx;
+    smt::kernel*                 m_ctx = nullptr;
     symbol                       m_logic;
-    progress_callback *          m_callback;
-    bool                         m_candidate_models;
-    bool                         m_fail_if_inconclusive;
+    progress_callback*           m_callback = nullptr;
+    bool                         m_candidate_models = false;
+    bool                         m_fail_if_inconclusive = false;
 
 public:
     smt_tactic(ast_manager& m, params_ref const & p):
         m(m),
         m_params_ref(p),
-        m_ctx(nullptr),
-        m_callback(nullptr),
         m_vars(m) {
         updt_params_core(p);
         TRACE("smt_tactic", tout << "p: " << p << "\n";);
@@ -66,6 +64,8 @@ public:
         SASSERT(m_ctx == nullptr);
     }
 
+    char const* name() const override { return "smt"; }
+
     smt_params & fparams() {
         return m_params;
     }
diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp
index 44086aa7e..97ce4a1c1 100644
--- a/src/smt/tactic/unit_subsumption_tactic.cpp
+++ b/src/smt/tactic/unit_subsumption_tactic.cpp
@@ -38,6 +38,8 @@ struct unit_subsumption_tactic : public tactic {
         m_clauses(m) {
     }
 
+    char const* name() const override { return "unit_subsumption"; }
+
     void cleanup() override {}
 
     void operator()(/* in */  goal_ref const & in, 
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 8336f0050..2f3ba7798 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -757,6 +757,8 @@ public:
         init();
     }
 
+    char const* name() const override { return "parallel_tactic"; }
+
     void operator()(const goal_ref & g,goal_ref_buffer & result) override {
         cleanup();
         fail_if_proof_generation("parallel-tactic", g);
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 8641a2aa8..389ee124b 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -186,6 +186,8 @@ public:
     tactic * translate(ast_manager & m) override {
         return alloc(solver2tactic, m_solver->translate(m, m_params));
     }    
+
+    char const* name() const override { return "solver2tactic"; }
 };
 
 tactic* mk_solver2tactic(solver* s) { return alloc(solver2tactic, s); }
diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp
index 7b80582fe..5ffc0dc20 100644
--- a/src/tactic/aig/aig_tactic.cpp
+++ b/src/tactic/aig/aig_tactic.cpp
@@ -45,6 +45,8 @@ public:
     aig_tactic(params_ref const & p = params_ref()):m_aig_manager(nullptr) {
         updt_params(p); 
     }
+
+    char const* name() const override { return "aig"; }
     
     tactic * translate(ast_manager & m) override {
         aig_tactic * t = alloc(aig_tactic);
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index b1367ea21..4493568bf 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -145,6 +145,8 @@ public:
     ~add_bounds_tactic() override {
         dealloc(m_imp);
     }
+
+    char const* name() const override { return "add_bounds"; }
     
     void updt_params(params_ref const & p) override {
         m_params = p;
diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp
index a8fcc4e00..87308078a 100644
--- a/src/tactic/arith/arith_bounds_tactic.cpp
+++ b/src/tactic/arith/arith_bounds_tactic.cpp
@@ -27,6 +27,8 @@ struct arith_bounds_tactic : public tactic {
                     /* out */ goal_ref_buffer & result) override {        
         bounds_arith_subsumption(in, result);
     }
+
+    char const* name() const override { return "arith_bounds"; }
     
     tactic* translate(ast_manager & mgr) override {
         return alloc(arith_bounds_tactic, mgr);
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 552270551..fce096f23 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -42,6 +42,8 @@ public:
     ~card2bv_tactic() override {
     }
 
+    char const* name() const override { return "card2bv"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
     }
diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp
index d3c5bb74c..e34910e78 100644
--- a/src/tactic/arith/degree_shift_tactic.cpp
+++ b/src/tactic/arith/degree_shift_tactic.cpp
@@ -284,6 +284,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "degree_shift"; }
+
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
         (*m_imp)(in, result);
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index a2ca66af2..92ce7cd29 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -357,6 +357,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "diff_neq"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 865c268a1..a1a1a56cc 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -268,6 +268,8 @@ public:
     tactic * translate(ast_manager & m) override {
         return alloc(eq2bv_tactic, m);
     }
+
+    char const* name() const override { return "eq2bv"; }
         
     void collect_param_descrs(param_descrs & r) override {
     }
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 7875aaf6d..07b59a3f9 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -294,6 +294,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "factor"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->m_rw.cfg().updt_params(p);
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index c5d119685..f2039c378 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -300,6 +300,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "fix_dl_var"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 4f10b0b3f..ef8109de0 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1642,6 +1642,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "fm"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index ae0467039..77786e267 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -132,6 +132,8 @@ public:
         dealloc(m_todo);
     }
 
+    char const* name() const override { return "lia2card"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_compile_equality = p.get_bool("compile_equality", true);
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 9af642e69..d67f49a37 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -305,6 +305,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "lia2pb"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 43def0741..887cc9e31 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -438,6 +438,8 @@ public:
     ~nla2bv_tactic() override {
     }
 
+    char const* name() const override { return "nla2bv"; }
+
     void updt_params(params_ref const & p) override {
 		m_params.append(p);
     }
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index 957859cc7..b7ef28f49 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -153,6 +153,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "normalize_bounds"; }
+
     void updt_params(params_ref const & p) override {
         m_imp->updt_params(p);
     }
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 98724923b..b63c85f1b 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -1007,6 +1007,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "pb2bv"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index f4169cfba..d55ea4ecf 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -49,6 +49,8 @@ public:
 
     ~propagate_ineqs_tactic() override;
 
+    char const* name() const override { return "propagate_ineqs"; }
+
     void updt_params(params_ref const & p) override;
     void collect_param_descrs(param_descrs & r) override {}
 
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 1691fe29a..db43a3ee6 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -903,6 +903,8 @@ public:
     ~purify_arith_tactic() override {
     }
 
+    char const* name() const override { return "purify_arith"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
     }
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index 7e1fe17ca..a7cef82e3 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -398,6 +398,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "recover_01"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 60dabbf5b..744f207f3 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -119,6 +119,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "bit_blaster"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index 9fd077599..3af58bf66 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -431,6 +431,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "bv1_blaster"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->m_rw.cfg().updt_params(p);
diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp
index baef6c4f2..e0b6e4d81 100644
--- a/src/tactic/bv/bv_bound_chk_tactic.cpp
+++ b/src/tactic/bv/bv_bound_chk_tactic.cpp
@@ -140,6 +140,7 @@ public:
     void cleanup() override;
     void collect_statistics(statistics & st) const override;
     void reset_statistics() override;
+    char const* name() const override { return "bv_bound_chk"; }
 };
 
 class bv_bound_chk_tactic::imp {
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index 5b9a4b21e..a9d15a2a6 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -54,6 +54,8 @@ public:
         return alloc(bv_size_reduction_tactic, m);
     }
 
+    char const* name() const override { return "bv_size"; }
+
     void operator()(goal_ref const & g, goal_ref_buffer & result) override;
 
     void cleanup() override {
diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp
index 0d1925a4a..d0bd6538b 100644
--- a/src/tactic/bv/bvarray2uf_tactic.cpp
+++ b/src/tactic/bv/bvarray2uf_tactic.cpp
@@ -113,6 +113,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "bvarray2uf"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index 3b18222af..4f9ae6e9d 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -104,6 +104,8 @@ public:
 
     dt2bv_tactic(ast_manager& m, params_ref const& p): 
         m(m), m_params(p), m_dt(m), m_bv(m), m_is_fd(*this) {}
+
+    char const* name() const override { return "dt2bv"; }
     
     tactic * translate(ast_manager & m) override {
         return alloc(dt2bv_tactic, m, m_params);
diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp
index 178a8fc77..7c72abde9 100644
--- a/src/tactic/bv/elim_small_bv_tactic.cpp
+++ b/src/tactic/bv/elim_small_bv_tactic.cpp
@@ -234,6 +234,8 @@ public:
         m_params(p) {
     }
 
+    char const* name() const override { return "elim_small_bv"; }
+
     tactic * translate(ast_manager & m) override {
         return alloc(elim_small_bv_tactic, m, m_params);
     }
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index 16e4b9679..0efe4f58c 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -277,6 +277,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "max_bv_sharing"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->m_rw.cfg().updt_params(p);
diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
index 97662a0c9..fe1269732 100644
--- a/src/tactic/core/blast_term_ite_tactic.cpp
+++ b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -171,6 +171,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "blast_term_ite"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->m_rw.m_cfg.updt_params(p);
diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp
index 8260d59c7..d1b8f5b1b 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.cpp
+++ b/src/tactic/core/cofactor_term_ite_tactic.cpp
@@ -51,6 +51,7 @@ public:
     }
 
     ~cofactor_term_ite_tactic() override {}
+    char const* name() const override { return "cofactor"; }
     void updt_params(params_ref const & p) override { m_params = p; m_elim_ite.updt_params(p); }
     void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); }
     
diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp
index b3c6d0e24..3d8ebfb12 100644
--- a/src/tactic/core/collect_statistics_tactic.cpp
+++ b/src/tactic/core/collect_statistics_tactic.cpp
@@ -53,6 +53,8 @@ public:
 
     ~collect_statistics_tactic() override {}
 
+    char const* name() const override { return "collect_statistics"; }
+
     tactic * translate(ast_manager & m_) override {
         return alloc(collect_statistics_tactic, m_, m_params);
     }
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index e7c1660c8..0beced06e 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -49,6 +49,8 @@ public:
 
     ~ctx_simplify_tactic() override;
 
+    char const* name() const override { return "ctx_simplify"; }
+
     void updt_params(params_ref const & p) override;
     static  void get_param_descrs(param_descrs & r);
     void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); }
diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp
index f26202015..011804803 100644
--- a/src/tactic/core/der_tactic.cpp
+++ b/src/tactic/core/der_tactic.cpp
@@ -68,6 +68,8 @@ public:
     ~der_tactic() override {
         dealloc(m_imp);
     }
+
+    char const* name() const override { return "der"; }
     
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp
index cb7eac498..1d171aae3 100644
--- a/src/tactic/core/distribute_forall_tactic.cpp
+++ b/src/tactic/core/distribute_forall_tactic.cpp
@@ -102,6 +102,8 @@ public:
         return alloc(distribute_forall_tactic);
     }
 
+    char const* name() const override { return "distribute_forall"; }
+
     void operator()(goal_ref const & g,
                     goal_ref_buffer & result) override {
         ast_manager & m = g->m();
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 719de8911..1dda062c8 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -182,6 +182,7 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) {
     return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params);
 }
 
+
 void dom_simplify_tactic::operator()(goal_ref const & in, goal_ref_buffer & result) {
     tactic_report report("dom-simplify", *in.get());
     simplify_goal(*(in.get()));
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 541d50838..b1f452d42 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -131,6 +131,8 @@ public:
 
     ~dom_simplify_tactic() override;
 
+    char const* dom_simplify_tactic::name() const { return "dom_simplify"; }
+
     tactic * translate(ast_manager & m) override;
     void updt_params(params_ref const & p) override {}
     static  void get_param_descrs(param_descrs & r) {}
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index c2d972b62..42adf04a9 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -136,6 +136,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "elim_term_ite"; }
+
     tactic * translate(ast_manager & m) override {
         return alloc(elim_term_ite_tactic, m, m_params);
     }
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 4df4d1fc4..915a0f3c0 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -853,6 +853,8 @@ public:
         updt_params(p);
     }
 
+   char const* name() const override { return "elim_uncstr"; }
+
     tactic * translate(ast_manager & m) override {
         return alloc(elim_uncnstr_tactic, m, m_params);
     }
diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index 82e78d771..485eda4dd 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -255,6 +255,8 @@ public:
         dealloc(m_map);
     }
 
+    char const* name() const override { return "injectivity"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_finder->updt_params(p);
diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp
index 72ebb949d..164cf9311 100644
--- a/src/tactic/core/nnf_tactic.cpp
+++ b/src/tactic/core/nnf_tactic.cpp
@@ -49,6 +49,8 @@ public:
 
     ~nnf_tactic() override {}
 
+    char const* name() const override { return "nnf"; }
+
     void updt_params(params_ref const & p) override { m_params = p; }
 
     void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); }
diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp
index b1f9d3f93..c3c027fef 100644
--- a/src/tactic/core/occf_tactic.cpp
+++ b/src/tactic/core/occf_tactic.cpp
@@ -196,6 +196,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "occf"; }
+
     void updt_params(params_ref const & p) override {}
     void collect_param_descrs(param_descrs & r) override {}
     
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 1d4805c67..ef3db804b 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -107,6 +107,8 @@ public:
     tactic * translate(ast_manager & m) override {
         return alloc(pb_preprocess_tactic, m);
     }
+
+    char const* name() const override { return "pb_preprocess"; }
     
     void operator()(
         goal_ref const & g, 
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 6cf340e57..b735de4b7 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -216,6 +216,8 @@ public:
         return alloc(propagate_values_tactic, m, m_params);
     }
 
+    char const* name() const override { return "propagate_values"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_r.updt_params(p);
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 8a1833bb4..e08593922 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -73,6 +73,8 @@ public:
     }
 
     ~reduce_args_tactic() override;
+
+    char const* name() const override { return "reduce_args"; }
     
     void operator()(goal_ref const & g, goal_ref_buffer & result) override;
     void cleanup() override;
@@ -86,15 +88,14 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
 
 struct reduce_args_tactic::imp {
     expr_ref_vector m_vars;
-    ast_manager &            m_manager;
+    ast_manager &            m;
     bv_util                  m_bv;
     array_util               m_ar;
 
-    ast_manager & m() const { return m_manager; }
     
     imp(ast_manager & m):
         m_vars(m),
-        m_manager(m),
+        m(m),
         m_bv(m),
         m_ar(m) {
     }
@@ -120,17 +121,17 @@ struct reduce_args_tactic::imp {
     }
 
     void checkpoint() { 
-        tactic::checkpoint(m_manager);
+        tactic::checkpoint(m);
     }
     
     struct find_non_candidates_proc {
-        ast_manager &              m_manager;
+        ast_manager &              m;
         bv_util &                  m_bv;
         array_util &               m_ar;
         obj_hashtable<func_decl> & m_non_candidates;
         
         find_non_candidates_proc(ast_manager & m, bv_util & bv, array_util& ar, obj_hashtable<func_decl> & non_candidates):
-            m_manager(m),
+            m(m),
             m_bv(bv),
             m_ar(ar),
             m_non_candidates(non_candidates) {
@@ -156,7 +157,7 @@ struct reduce_args_tactic::imp {
             unsigned j    = n->get_num_args();        
             while (j > 0) {
                 --j;
-                if (may_be_unique(m_manager, m_bv, n->get_arg(j)))
+                if (may_be_unique(m, m_bv, n->get_arg(j)))
                     return;
             }  
             m_non_candidates.insert(d);
@@ -172,7 +173,7 @@ struct reduce_args_tactic::imp {
         for (expr* v : m_vars)
             if (is_app(v))
                 non_candidates.insert(to_app(v)->get_decl());
-        find_non_candidates_proc proc(m_manager, m_bv, m_ar, non_candidates);
+        find_non_candidates_proc proc(m, m_bv, m_ar, non_candidates);
         expr_fast_mark1 visited;
         unsigned sz = g.size();
         for (unsigned i = 0; i < sz; i++) {
@@ -187,14 +188,14 @@ struct reduce_args_tactic::imp {
     }
 
     struct populate_decl2args_proc {
-        ast_manager &                     m_manager;
+        ast_manager &                     m;
         bv_util &                         m_bv;
         obj_hashtable<func_decl> &        m_non_candidates;
         obj_map<func_decl, bit_vector> &  m_decl2args;    
         obj_map<func_decl, svector<expr*> > m_decl2base; // for args = base + offset
 
         populate_decl2args_proc(ast_manager & m, bv_util & bv, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & d):
-            m_manager(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {}
+            m(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {}
         
         void operator()(var * n) {}
         void operator()(quantifier * n) {}
@@ -218,7 +219,7 @@ struct reduce_args_tactic::imp {
                 it->m_value.reserve(j);
                 while (j > 0) {
                     --j;
-                    it->m_value.set(j, may_be_unique(m_manager, m_bv, n->get_arg(j), base));
+                    it->m_value.set(j, may_be_unique(m, m_bv, n->get_arg(j), base));
                     bases[j] = base;
                 }
             } else {
@@ -226,7 +227,7 @@ struct reduce_args_tactic::imp {
                 SASSERT(j == it->m_value.size());                        
                 while (j > 0) {
                     --j;
-                    it->m_value.set(j, it->m_value.get(j) && may_be_unique(m_manager, m_bv, n->get_arg(j), base) && bases[j] == base);
+                    it->m_value.set(j, it->m_value.get(j) && may_be_unique(m, m_bv, n->get_arg(j), base) && bases[j] == base);
                 }
             }
         }
@@ -237,7 +238,7 @@ struct reduce_args_tactic::imp {
                             obj_map<func_decl, bit_vector> & decl2args) {
         expr_fast_mark1 visited;
         decl2args.reset();
-        populate_decl2args_proc proc(m_manager, m_bv, non_candidates, decl2args);
+        populate_decl2args_proc proc(m, m_bv, non_candidates, decl2args);
         unsigned sz = g.size();
         for (unsigned i = 0; i < sz; i++) {
             checkpoint();
@@ -246,28 +247,24 @@ struct reduce_args_tactic::imp {
         
         // Remove all cases where the simplification is not applicable.
         ptr_buffer<func_decl> bad_decls;
-        obj_map<func_decl, bit_vector>::iterator it  = decl2args.begin();
-        obj_map<func_decl, bit_vector>::iterator end = decl2args.end();
-        for (; it != end; it++) {
+        for (auto const& [k, v] : decl2args) {
             bool is_zero = true;
-            for (unsigned i = 0; i < it->m_value.size() && is_zero ; i++) {
-                if (it->m_value.get(i)) 
+            for (unsigned i = 0; i < v.size() && is_zero; i++) {
+                if (v.get(i))
                     is_zero = false;
             }
-            if (is_zero) 
-                bad_decls.push_back(it->m_key);
+            if (is_zero)
+                bad_decls.push_back(k);
         }
     
-        ptr_buffer<func_decl>::iterator it2  = bad_decls.begin();
-        ptr_buffer<func_decl>::iterator end2 = bad_decls.end();
-        for (; it2 != end2; ++it2)
-            decl2args.erase(*it2);
+        for (func_decl* a : bad_decls)
+            decl2args.erase(a);
 
         TRACE("reduce_args", tout << "decl2args:" << std::endl;
-              for (obj_map<func_decl, bit_vector>::iterator it = decl2args.begin() ; it != decl2args.end() ; it++) {
-                  tout << it->m_key->get_name() << ": ";
-                  for (unsigned i = 0 ; i < it->m_value.size() ; i++)
-                      tout << (it->m_value.get(i) ? "1" : "0");                            
+              for (auto const& [k, v] : decl2args) {
+                  tout << k->get_name() << ": ";
+                  for (auto b : v)
+                      tout << (b ? "1" : "0");                            
                   tout << std::endl;
               });
     }
@@ -311,22 +308,17 @@ struct reduce_args_tactic::imp {
     typedef obj_map<func_decl, arg2func *> decl2arg2func_map;
 
     struct reduce_args_ctx { 
-        ast_manager &           m_manager;
+        ast_manager &           m;
         decl2arg2func_map       m_decl2arg2funcs;
 
-        reduce_args_ctx(ast_manager & m): m_manager(m) {
+        reduce_args_ctx(ast_manager & m): m(m) {
         }
         
         ~reduce_args_ctx() {
-            obj_map<func_decl, arg2func *>::iterator it  = m_decl2arg2funcs.begin();
-            obj_map<func_decl, arg2func *>::iterator end = m_decl2arg2funcs.end();
-            for (; it != end; ++it) {
-                arg2func * map = it->m_value;
-                arg2func::iterator it2  = map->begin();
-                arg2func::iterator end2 = map->end();
-                for (; it2 != end2; ++it2) {
-                    m_manager.dec_ref(it2->m_key);
-                    m_manager.dec_ref(it2->m_value);
+            for (auto const& [_, map] : m_decl2arg2funcs) {
+                for (auto const& [k, v] : *map) {
+                    m.dec_ref(k);
+                    m.dec_ref(v);
                 }
                 dealloc(map);
             }
@@ -340,7 +332,7 @@ struct reduce_args_tactic::imp {
         decl2arg2func_map &              m_decl2arg2funcs;
         
         reduce_args_rw_cfg(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
-            m(owner.m_manager),
+            m(owner.m),
             m_owner(owner),
             m_decl2args(decl2args),
             m_decl2arg2funcs(decl2arg2funcs) {
@@ -396,16 +388,16 @@ struct reduce_args_tactic::imp {
         reduce_args_rw_cfg m_cfg;
     public:
         reduce_args_rw(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
-            rewriter_tpl<reduce_args_rw_cfg>(owner.m_manager, false, m_cfg),
+            rewriter_tpl<reduce_args_rw_cfg>(owner.m, false, m_cfg),
             m_cfg(owner, decl2args, decl2arg2funcs) {
         }
     };
 
     model_converter * mk_mc(obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs) {
         ptr_buffer<expr> new_args;
-        var_ref_vector   new_vars(m_manager);
+        var_ref_vector   new_vars(m);
         ptr_buffer<expr> new_eqs;
-        generic_model_converter * f_mc    = alloc(generic_model_converter, m_manager, "reduce_args");
+        generic_model_converter * f_mc    = alloc(generic_model_converter, m, "reduce_args");
         for (auto const& kv : decl2arg2funcs) {
             func_decl * f  = kv.m_key;
             arg2func * map = kv.m_value;
@@ -415,18 +407,14 @@ struct reduce_args_tactic::imp {
             new_vars.reset();
             new_args.reset();
             for (unsigned i = 0; i < f->get_arity(); i++) {
-                new_vars.push_back(m_manager.mk_var(i, f->get_domain(i)));
+                new_vars.push_back(m.mk_var(i, f->get_domain(i)));
                 if (!bv.get(i))
                     new_args.push_back(new_vars.back());
             }
-            arg2func::iterator it2  = map->begin();
-            arg2func::iterator end2 = map->end();
-            for (; it2 != end2; ++it2) {
-                app * t = it2->m_key;
-                func_decl * new_def = it2->m_value;
+            for (auto const& [t, new_def] : *map) {
                 f_mc->hide(new_def);
                 SASSERT(new_def->get_arity() == new_args.size());
-                app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.data());
+                app * new_t = m.mk_app(new_def, new_args.size(), new_args.data());
                 if (def == nullptr) {
                     def = new_t;
                 }
@@ -434,15 +422,15 @@ struct reduce_args_tactic::imp {
                     new_eqs.reset();
                     for (unsigned i = 0; i < f->get_arity(); i++) {
                         if (bv.get(i))
-                            new_eqs.push_back(m_manager.mk_eq(new_vars.get(i), t->get_arg(i)));
+                            new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i)));
                     }
                     SASSERT(new_eqs.size() > 0);
                     expr * cond;
                     if (new_eqs.size() == 1)
                         cond = new_eqs[0];
                     else
-                        cond = m_manager.mk_and(new_eqs.size(), new_eqs.data());
-                    def = m_manager.mk_ite(cond, new_t, def);
+                        cond = m.mk_and(new_eqs.size(), new_eqs.data());
+                    def = m.mk_ite(cond, new_t, def);
                 }
             }
             SASSERT(def);
@@ -464,7 +452,7 @@ struct reduce_args_tactic::imp {
         if (decl2args.empty())
             return;
         
-        reduce_args_ctx ctx(m_manager);
+        reduce_args_ctx ctx(m);
         reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs);
         
         unsigned sz = g.size();
@@ -472,7 +460,7 @@ struct reduce_args_tactic::imp {
             if (g.inconsistent())
                 break;
             expr * f = g.form(i);
-            expr_ref new_f(m_manager);
+            expr_ref new_f(m);
             rw(f, new_f);
             g.update(i, new_f);
         }
@@ -499,7 +487,7 @@ void reduce_args_tactic::operator()(goal_ref const & g,
                                     goal_ref_buffer & result) {
     fail_if_unsat_core_generation("reduce-args", g);
     result.reset();
-    if (!m_imp->m().proofs_enabled()) {
+    if (!m_imp->m.proofs_enabled()) {
         m_imp->operator()(*(g.get()));
     }
     g->inc_depth();
@@ -507,7 +495,7 @@ void reduce_args_tactic::operator()(goal_ref const & g,
 }
 
 void reduce_args_tactic::cleanup() {
-    ast_manager & m   = m_imp->m();
+    ast_manager & m   = m_imp->m;
     expr_ref_vector vars = m_imp->m_vars;
     m_imp->~imp();
     m_imp = new (m_imp) imp(m);
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index a60f20aab..cfcc42482 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -47,6 +47,8 @@ public:
 
     ~reduce_invertible_tactic() override { }
 
+    char const* name() const override { return "reduce_invertible"; }
+
     tactic * translate(ast_manager & m) override {
         return alloc(reduce_invertible_tactic, m);
     }
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index 9fff34190..fc262f998 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/src/tactic/core/simplify_tactic.h
@@ -43,6 +43,8 @@ public:
 
     tactic * translate(ast_manager & m) override { return alloc(simplify_tactic, m, m_params); }
 
+    char const* name() const override { return "simplify"; }
+
 };
 
 tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index b9feaf949..9d844b7ed 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -1089,6 +1089,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "solve_eqs"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h
index 6bb72852d..a1cafb7c0 100644
--- a/src/tactic/core/special_relations_tactic.h
+++ b/src/tactic/core/special_relations_tactic.h
@@ -59,6 +59,8 @@ public:
 
     tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); }
 
+    char const* name() const override { return "special_relations"; }
+
 };
 
 tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref());
diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp
index 453e4a218..12b76b638 100644
--- a/src/tactic/core/split_clause_tactic.cpp
+++ b/src/tactic/core/split_clause_tactic.cpp
@@ -91,6 +91,8 @@ public:
     ~split_clause_tactic() override {
     }
 
+    char const* name() const override { return "split_clause"; }
+
     void updt_params(params_ref const & p) override {
         m_largest_clause = p.get_bool("split_largest_clause", false);
     }
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 17049e2d1..9aa4c9448 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -37,6 +37,8 @@ public:
     }
     
     ~symmetry_reduce_tactic() override;
+
+    char const* name() const override { return "symmetry_reduce"; }
     
     void operator()(goal_ref const & g, 
                     goal_ref_buffer & result) override;
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index b466c50fb..e26fded8f 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -891,6 +891,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "tseitin_cnf"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 13cb4c3e7..be98dea00 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -120,6 +120,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "fp2bv"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp
index 3a23f5984..b2591f05c 100644
--- a/src/tactic/portfolio/solver_subsumption_tactic.cpp
+++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp
@@ -133,6 +133,8 @@ public:
 
     ~solver_subsumption_tactic() override {}
 
+    char const* name() const override { return "solver_subsumption"; }
+
     void updt_params(params_ref const& p) override { 
         m_params = p; 
         unsigned max_conflicts = p.get_uint("max_conflicts", 2);
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index fd0dcaa3b..ece6940f3 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -50,6 +50,8 @@ public:
         dealloc(m_engine);
     }
 
+    char const* name() const override { return "sls"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_engine->updt_params(p);
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index ad9e8b46f..57c6ae99a 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -53,6 +53,8 @@ public:
 
     ~qfufbv_ackr_tactic() override { }
 
+    char const* name() const override { return "qfufbv_ackr"; }
+
     void operator()(goal_ref const & g, goal_ref_buffer & result) override {
         ast_manager& m(g->m());
         tactic_report report("qfufbv_ackr", *g);
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 66f58f71e..575435904 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -90,6 +90,8 @@ public:
 
     void cleanup() override {}
 
+    char const* name() const override { return "fail"; }
+
     tactic * translate(ast_manager & m) override { return this; }
 };
 
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 891f44ef1..7f7f293af 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -86,6 +86,7 @@ public:
     }
 
     unsigned user_propagate_register(expr* e) override { return 0; }
+    virtual char const* name() const = 0;
 
 protected:
     friend class nary_tactical;
@@ -116,6 +117,7 @@ public:
     void operator()(goal_ref const & in, goal_ref_buffer& result) override;
     void cleanup() override {}
     tactic * translate(ast_manager & m) override { return this; } 
+    char const* name() const { return "skip"; }
 };
 
 tactic * mk_skip_tactic();
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index c6419d95f..19009aa44 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -100,6 +100,8 @@ class and_then_tactical : public binary_tactical {
 public:
     and_then_tactical(tactic * t1, tactic * t2):binary_tactical(t1, t2) {}
 
+    char const* name() const override { return "and_then"; }
+
     void operator()(goal_ref const & in, goal_ref_buffer& result) override { 
 
         bool proofs_enabled = in->proofs_enabled();
@@ -313,6 +315,8 @@ class or_else_tactical : public nary_tactical {
 public:
     or_else_tactical(unsigned num, tactic * const * ts):nary_tactical(num, ts) { SASSERT(num > 0); }
 
+    char const* name() const override { return "or_else"; }
+
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         goal orig(*(in.get()));
         unsigned sz = m_ts.size();
@@ -414,6 +418,8 @@ public:
 		error_code = 0;
 	}
 
+    char const* name() const override { return "par"; }
+
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         bool use_seq;
         use_seq = false;
@@ -550,6 +556,8 @@ class par_and_then_tactical : public and_then_tactical {
 public:
     par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {}
 
+    char const* name() const override { return "par_then"; }
+
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         bool use_seq;
         use_seq = false;
@@ -915,6 +923,8 @@ public:
         unary_tactical(t), 
         m_max_depth(max_depth) {
     }
+
+    char const* name() const override { return "repeat"; }
     
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         operator()(0, in, result);
@@ -935,6 +945,8 @@ class fail_if_branching_tactical : public unary_tactical {
 public:
     fail_if_branching_tactical(tactic * t, unsigned threshold):unary_tactical(t), m_threshold(threshold) {}
 
+    char const* name() const override { return "fail_if_branching"; }
+
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         m_t->operator()(in, result);
         if (result.size() > m_threshold) {
@@ -957,6 +969,8 @@ class cleanup_tactical : public unary_tactical {
 public:
     cleanup_tactical(tactic * t):unary_tactical(t) {}
 
+    char const* name() const override { return "cleanup"; }
+
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         m_t->operator()(in, result);
         m_t->cleanup();
@@ -976,6 +990,8 @@ class try_for_tactical : public unary_tactical {
     unsigned m_timeout;
 public:
     try_for_tactical(tactic * t, unsigned ts):unary_tactical(t), m_timeout(ts) {}
+
+    char const* name() const override { return "try_for"; }
     
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         cancel_eh<reslimit> eh(in->m().limit());
@@ -1003,6 +1019,8 @@ public:
         t->updt_params(p);
     }
 
+    char const* name() const override { return "using_params"; }
+
     void updt_params(params_ref const & p) override {
         TRACE("using_params", 
               tout << "before p: " << p << "\n";
@@ -1052,6 +1070,8 @@ public:
         tactic * new_t = m_t->translate(m);
         return alloc(annotate_tactical, m_name.c_str(), new_t);
     }
+
+    char const* name() const override { return "annotate"; }
     
 };
 
@@ -1067,6 +1087,8 @@ public:
         m_p(p) { 
         SASSERT(m_p);
     }
+
+    char const* name() const override { return "cond"; }
     
     void operator()(goal_ref const & in, goal_ref_buffer & result) override {
         if (m_p->operator()(*(in.get())).is_true()) 
@@ -1098,6 +1120,8 @@ public:
         SASSERT(m_p);
     }
 
+    char const* name() const override { return "fail_if"; }
+
     void cleanup() override {}
 
     void  operator()(goal_ref const & in, goal_ref_buffer& result) override {
@@ -1123,6 +1147,8 @@ tactic * fail_if_not(probe * p) {
 class if_no_proofs_tactical : public unary_tactical {
 public:
     if_no_proofs_tactical(tactic * t):unary_tactical(t) {}
+
+    char const* name() const override { return "if_no_proofs"; }
     
     void operator()(goal_ref const & in, goal_ref_buffer & result) override {
         if (in->proofs_enabled()) {
@@ -1139,6 +1165,8 @@ public:
 class if_no_unsat_cores_tactical : public unary_tactical {
 public:
     if_no_unsat_cores_tactical(tactic * t):unary_tactical(t) {}
+
+    char const* name() const override { return "if_no_unsat_cores"; }
     
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (in->unsat_core_enabled()) {
@@ -1155,6 +1183,8 @@ public:
 class if_no_models_tactical : public unary_tactical {
 public:
     if_no_models_tactical(tactic * t):unary_tactical(t) {}
+
+    char const* name() const override { return "if_no_models"; }
     
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (in->models_enabled()) {
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 86c606538..c5745d85c 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -105,6 +105,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "macro_finder"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 33c2927bb..0e0cb7cb2 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -100,6 +100,8 @@ public:
         dealloc(m_imp);
     }
 
+    char const* name() const override { return "quasi_macros"; }
+
     void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index bb2b4d5be..d5bfec8fe 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -28,6 +28,8 @@ public:
     ufbv_rewriter_tactic(ast_manager & m, params_ref const & p):
         m_manager(m), m_params(p) {}
 
+    char const* name() const override { return "ufbv"; }
+
     tactic * translate(ast_manager & m) override {
         return alloc(ufbv_rewriter_tactic, m, m_params);
     }