diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index e2fbe81fa..8ebbe9cb4 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -129,17 +129,14 @@ public:
         m_trail(m), m_args(m), 
         m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {}
 
-
     virtual ~dom_simplify_tactic();
 
-    virtual tactic * translate(ast_manager & m);
-    virtual void updt_params(params_ref const & p) {}
+    tactic * translate(ast_manager & m) override;
+    void updt_params(params_ref const & p) override {}
     static  void get_param_descrs(param_descrs & r) {}
-    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
-    
+    void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); }    
     void operator()(goal_ref const & in, goal_ref_buffer & result) override;
-
-    virtual void cleanup();
+    void cleanup() override;
 };
 
 class expr_substitution_simplifier : public dom_simplifier {
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index 49815b6d1..c8591840d 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -136,33 +136,33 @@ public:
         m_params(p) {
         m_imp = alloc(imp, m, p);
     }
-
-    virtual tactic * translate(ast_manager & m) {
-        return alloc(elim_term_ite_tactic, m, m_params);
-    }
         
     virtual ~elim_term_ite_tactic() {
         dealloc(m_imp);
     }
 
-    virtual void updt_params(params_ref const & p) {
+    tactic * translate(ast_manager & m) override {
+        return alloc(elim_term_ite_tactic, m, m_params);
+    }
+
+    void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->m_rw.cfg().updt_params(p);
     }
 
-    virtual void collect_param_descrs(param_descrs & r) {
+    void collect_param_descrs(param_descrs & r) override {
         insert_max_memory(r);
         insert_max_steps(r);
         r.insert("max_args", CPK_UINT, 
                  "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
     }
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result) {
+    void operator()(goal_ref const & in, 
+                    goal_ref_buffer & result) override {
         (*m_imp)(in, result);
     }
     
-    virtual void cleanup() {
+    void cleanup() override {
         ast_manager & m = m_imp->m;
         m_imp->~imp();
         m_imp = new (m_imp) imp(m, m_params);
diff --git a/src/tactic/dependency_converter.cpp b/src/tactic/dependency_converter.cpp
index fbd445d52..34c864526 100644
--- a/src/tactic/dependency_converter.cpp
+++ b/src/tactic/dependency_converter.cpp
@@ -36,7 +36,7 @@ public:
     }
 
     virtual void display(std::ostream& out) {
-        out << m_dep << "\n";
+        out << m_dep.get() << "\n";
     }
 };