diff --git a/src/library/tactic/backward/backward_lemmas.cpp b/src/library/tactic/backward/backward_lemmas.cpp
index 35282d51db..69e86c7ce4 100644
--- a/src/library/tactic/backward/backward_lemmas.cpp
+++ b/src/library/tactic/backward/backward_lemmas.cpp
@@ -135,8 +135,8 @@ struct vm_backward_lemmas : public vm_external {
     vm_backward_lemmas(backward_lemma_index const & v):m_val(v) {}
     virtual ~vm_backward_lemmas() {}
     virtual void dealloc() override { this->~vm_backward_lemmas(); get_vm_allocator().deallocate(sizeof(vm_backward_lemmas), this); }
-    virtual vm_external * ts_clone() { return new vm_backward_lemmas(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_backward_lemmas))) vm_backward_lemmas(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_backward_lemmas(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_backward_lemmas))) vm_backward_lemmas(m_val); }
 };
 
 backward_lemma_index const & to_backward_lemmas(vm_obj const & o) {
diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index 7b1c901e84..41f232b2ca 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -1240,8 +1240,8 @@ struct vm_simp_lemmas : public vm_external {
     vm_simp_lemmas(simp_lemmas const & v): m_val(v) {}
     virtual ~vm_simp_lemmas() {}
     virtual void dealloc() override { this->~vm_simp_lemmas(); get_vm_allocator().deallocate(sizeof(vm_simp_lemmas), this); }
-    virtual vm_external * ts_clone() { return new vm_simp_lemmas(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_simp_lemmas))) vm_simp_lemmas(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_simp_lemmas(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_simp_lemmas))) vm_simp_lemmas(m_val); }
 };
 
 bool is_simp_lemmas(vm_obj const & o) {
diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp
index 136e3a0468..12cf2f24c5 100644
--- a/src/library/tactic/smt/congruence_tactics.cpp
+++ b/src/library/tactic/smt/congruence_tactics.cpp
@@ -28,8 +28,8 @@ struct vm_cc_state : public vm_external {
     virtual void dealloc() override {
         this->~vm_cc_state(); get_vm_allocator().deallocate(sizeof(vm_cc_state), this);
     }
-    virtual vm_external * ts_clone() { return new vm_cc_state(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_cc_state))) vm_cc_state(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_cc_state(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_cc_state))) vm_cc_state(m_val); }
 };
 
 bool is_cc_state(vm_obj const & o) {
diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp
index 1139e2c856..8f82236223 100644
--- a/src/library/tactic/smt/ematch.cpp
+++ b/src/library/tactic/smt/ematch.cpp
@@ -1018,8 +1018,8 @@ struct vm_ematch_state : public vm_external {
     vm_ematch_state(ematch_state const & v): m_val(v) {}
     virtual ~vm_ematch_state() {}
     virtual void dealloc() override { this->~vm_ematch_state(); get_vm_allocator().deallocate(sizeof(vm_ematch_state), this); }
-    virtual vm_external * ts_clone() { return new vm_ematch_state(m_val); }
-    virtual vm_external * clone()  { return new (get_vm_allocator().allocate(sizeof(vm_ematch_state))) vm_ematch_state(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_ematch_state(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_ematch_state))) vm_ematch_state(m_val); }
 };
 
 ematch_state const & to_ematch_state(vm_obj const & o) {
diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp
index 91ca52674a..70e404dc71 100644
--- a/src/library/tactic/smt/hinst_lemmas.cpp
+++ b/src/library/tactic/smt/hinst_lemmas.cpp
@@ -687,8 +687,8 @@ struct vm_hinst_lemma : public vm_external {
     vm_hinst_lemma(hinst_lemma const & v): m_val(v) {}
     virtual ~vm_hinst_lemma() {}
     virtual void dealloc() override { this->~vm_hinst_lemma(); get_vm_allocator().deallocate(sizeof(vm_hinst_lemma), this); }
-    virtual vm_external * ts_clone() { return new vm_hinst_lemma(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_hinst_lemma))) vm_hinst_lemma(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_hinst_lemma(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_hinst_lemma))) vm_hinst_lemma(m_val); }
 };
 
 hinst_lemma const & to_hinst_lemma(vm_obj const & o) {
@@ -733,8 +733,8 @@ struct vm_hinst_lemmas : public vm_external {
     vm_hinst_lemmas(hinst_lemmas const & v): m_val(v) {}
     virtual ~vm_hinst_lemmas() {}
     virtual void dealloc() override { this->~vm_hinst_lemmas(); get_vm_allocator().deallocate(sizeof(vm_hinst_lemmas), this); }
-    virtual vm_external * ts_clone() { return new vm_hinst_lemmas(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_hinst_lemmas))) vm_hinst_lemmas(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_hinst_lemmas(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_hinst_lemmas))) vm_hinst_lemmas(m_val); }
 };
 
 hinst_lemmas const & to_hinst_lemmas(vm_obj const & o) {
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index ef6b4fb8f2..3c2ed72d3d 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -116,8 +116,8 @@ struct vm_smt_goal : public vm_external {
     virtual void dealloc() override {
         this->~vm_smt_goal(); get_vm_allocator().deallocate(sizeof(vm_smt_goal), this);
     }
-    virtual vm_external * ts_clone() { return new vm_smt_goal(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_smt_goal))) vm_smt_goal(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_smt_goal(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_smt_goal))) vm_smt_goal(m_val); }
 };
 
 bool is_smt_goal(vm_obj const & o) {
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index ccb40149c2..3935e13030 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -212,8 +212,8 @@ struct vm_tactic_state : public vm_external {
     virtual void dealloc() override {
         this->~vm_tactic_state(); get_vm_allocator().deallocate(sizeof(vm_tactic_state), this);
     }
-    virtual vm_external * ts_clone() { return new vm_tactic_state(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_tactic_state))) vm_tactic_state(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_tactic_state(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_tactic_state))) vm_tactic_state(m_val); }
 };
 
 bool is_tactic_state(vm_obj const & o) {
diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp
index c53fac8bf1..665719fedd 100644
--- a/src/library/tactic/vm_monitor.cpp
+++ b/src/library/tactic/vm_monitor.cpp
@@ -176,8 +176,8 @@ struct vm_vm_decl : public vm_external {
     vm_vm_decl(vm_decl const & v):m_val(v) {}
     virtual ~vm_vm_decl() {}
     virtual void dealloc() override { this->~vm_vm_decl(); get_vm_allocator().deallocate(sizeof(vm_vm_decl), this); }
-    virtual vm_external * ts_clone() { return new vm_vm_decl(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_vm_decl))) vm_vm_decl(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_vm_decl(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_vm_decl))) vm_vm_decl(m_val); }
 };
 
 vm_decl const & to_vm_decl(vm_obj const & o) {
diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp
index b40a819fca..01334e9458 100644
--- a/src/library/vm/vm_declaration.cpp
+++ b/src/library/vm/vm_declaration.cpp
@@ -43,8 +43,8 @@ struct vm_declaration : public vm_external {
     vm_declaration(declaration const & v):m_val(v) {}
     virtual ~vm_declaration() {}
     virtual void dealloc() override { this->~vm_declaration(); get_vm_allocator().deallocate(sizeof(vm_declaration), this); }
-    virtual vm_external * ts_clone() { return new vm_declaration(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_declaration))) vm_declaration(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_declaration(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_declaration))) vm_declaration(m_val); }
 };
 
 bool is_declaration(vm_obj const & o) {
diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp
index 0d2a44f05b..2a9723222a 100644
--- a/src/library/vm/vm_environment.cpp
+++ b/src/library/vm/vm_environment.cpp
@@ -29,8 +29,8 @@ struct vm_environment : public vm_external {
     vm_environment(environment const & v):m_val(v) {}
     virtual ~vm_environment() {}
     virtual void dealloc() override { this->~vm_environment(); get_vm_allocator().deallocate(sizeof(vm_environment), this); }
-    virtual vm_external * ts_clone() { return new vm_environment(m_val); }
-    virtual vm_external * clone()  { return new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_environment(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(m_val); }
 };
 
 bool is_env(vm_obj const & o) {
diff --git a/src/library/vm/vm_exceptional.cpp b/src/library/vm/vm_exceptional.cpp
index 815ee6716f..22085d1a3c 100644
--- a/src/library/vm/vm_exceptional.cpp
+++ b/src/library/vm/vm_exceptional.cpp
@@ -16,8 +16,8 @@ struct vm_throwable : public vm_external {
     vm_throwable(throwable const & ex):m_val(ex.clone()) {}
     virtual ~vm_throwable() { delete m_val; }
     virtual void dealloc() override { this->~vm_throwable(); get_vm_allocator().deallocate(sizeof(vm_throwable), this); }
-    virtual vm_external * ts_clone() { return new vm_throwable(*m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_throwable))) vm_throwable(*m_val); }
+    virtual vm_external * ts_clone() override { return new vm_throwable(*m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_throwable))) vm_throwable(*m_val); }
 };
 
 throwable * to_throwable(vm_obj const & o) {
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index e18004c4b5..9e6175562f 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -36,8 +36,8 @@ struct vm_macro_definition : public vm_external {
     virtual void dealloc() override {
         this->~vm_macro_definition(); get_vm_allocator().deallocate(sizeof(vm_macro_definition), this);
     }
-    virtual vm_external * ts_clone() { return new vm_macro_definition(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_macro_definition))) vm_macro_definition(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_macro_definition(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_macro_definition))) vm_macro_definition(m_val); }
 };
 
 macro_definition const & to_macro_definition(vm_obj const & o) {
@@ -55,8 +55,8 @@ struct vm_expr : public vm_external {
     vm_expr(expr const & v):m_val(v) {}
     virtual ~vm_expr() {}
     virtual void dealloc() override { this->~vm_expr(); get_vm_allocator().deallocate(sizeof(vm_expr), this); }
-    virtual vm_external * ts_clone() { return new vm_expr(m_val); }
-    virtual vm_external * clone()  { return new (get_vm_allocator().allocate(sizeof(vm_expr))) vm_expr(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_expr(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_expr))) vm_expr(m_val); }
 };
 
 bool is_expr(vm_obj const & o) {
diff --git a/src/library/vm/vm_format.cpp b/src/library/vm/vm_format.cpp
index 063b99a716..0d0380fc89 100644
--- a/src/library/vm/vm_format.cpp
+++ b/src/library/vm/vm_format.cpp
@@ -19,8 +19,8 @@ struct vm_format : public vm_external {
     vm_format(format const & v):m_val(v) {}
     virtual ~vm_format() {}
     virtual void dealloc() override { this->~vm_format(); get_vm_allocator().deallocate(sizeof(vm_format), this); }
-    virtual vm_external * ts_clone() { return new vm_format(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_format))) vm_format(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_format(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_format))) vm_format(m_val); }
 };
 
 bool is_format(vm_obj const & o) {
@@ -119,8 +119,8 @@ struct vm_format_thunk : public vm_external {
     vm_format_thunk(std::function<format()> const & fn):m_val(fn) {}
     virtual ~vm_format_thunk() {}
     virtual void dealloc() override { this->~vm_format_thunk(); get_vm_allocator().deallocate(sizeof(vm_format_thunk), this); }
-    virtual vm_external * ts_clone() { return new vm_format_thunk(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_format_thunk))) vm_format_thunk(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_format_thunk(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_format_thunk))) vm_format_thunk(m_val); }
 };
 
 std::function<format()> const & to_format_thunk(vm_obj const & o) {
diff --git a/src/library/vm/vm_level.cpp b/src/library/vm/vm_level.cpp
index 65fd3172b4..3fc9418f57 100644
--- a/src/library/vm/vm_level.cpp
+++ b/src/library/vm/vm_level.cpp
@@ -20,8 +20,8 @@ struct vm_level : public vm_external {
     vm_level(level const & v):m_val(v) {}
     virtual ~vm_level() {}
     virtual void dealloc() override { this->~vm_level(); get_vm_allocator().deallocate(sizeof(vm_level), this); }
-    virtual vm_external * ts_clone() { return new vm_level(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_level))) vm_level(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_level(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_level))) vm_level(m_val); }
 };
 
 bool is_level(vm_obj const & o) {
diff --git a/src/library/vm/vm_list.cpp b/src/library/vm/vm_list.cpp
index 951b4c30c3..721ba7f235 100644
--- a/src/library/vm/vm_list.cpp
+++ b/src/library/vm/vm_list.cpp
@@ -19,8 +19,8 @@ struct vm_list : public vm_external {
     virtual void dealloc() override {
         this->~vm_list(); get_vm_allocator().deallocate(sizeof(vm_list<A>), this);
     }
-    virtual vm_external * ts_clone() { return new vm_list<A>(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_list<A>))) vm_list<A>(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_list<A>(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_list<A>))) vm_list<A>(m_val); }
 };
 
 template<typename A>
diff --git a/src/library/vm/vm_name.cpp b/src/library/vm/vm_name.cpp
index b2533dabc8..381a41b157 100644
--- a/src/library/vm/vm_name.cpp
+++ b/src/library/vm/vm_name.cpp
@@ -18,8 +18,8 @@ struct vm_name : public vm_external {
     vm_name(name const & v):m_val(v) {}
     virtual ~vm_name() {}
     virtual void dealloc() override { this->~vm_name(); get_vm_allocator().deallocate(sizeof(vm_name), this); }
-    virtual vm_external * ts_clone() { return new vm_name(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_name))) vm_name(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_name(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_name))) vm_name(m_val); }
 };
 
 bool is_name(vm_obj const & o) {
diff --git a/src/library/vm/vm_options.cpp b/src/library/vm/vm_options.cpp
index 095dd316c9..dbd35ea83a 100644
--- a/src/library/vm/vm_options.cpp
+++ b/src/library/vm/vm_options.cpp
@@ -17,8 +17,8 @@ struct vm_options : public vm_external {
     vm_options(options const & v):m_val(v) {}
     virtual ~vm_options() {}
     virtual void dealloc() override { this->~vm_options(); get_vm_allocator().deallocate(sizeof(vm_options), this); }
-    virtual vm_external * ts_clone() { return new vm_options(m_val); }
-    virtual vm_external * clone()  { return new (get_vm_allocator().allocate(sizeof(vm_options))) vm_options(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_options(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_options))) vm_options(m_val); }
 };
 
 options const & to_options(vm_obj const & o) {
diff --git a/src/library/vm/vm_rb_map.cpp b/src/library/vm/vm_rb_map.cpp
index 2abcb40662..8504282e1c 100644
--- a/src/library/vm/vm_rb_map.cpp
+++ b/src/library/vm/vm_rb_map.cpp
@@ -28,8 +28,8 @@ struct vm_rb_map : public vm_external {
     vm_rb_map(vm_obj_map const & m):m_map(m) {}
     virtual ~vm_rb_map() {}
     virtual void dealloc() override { this->~vm_rb_map(); get_vm_allocator().deallocate(sizeof(vm_rb_map), this); }
-    virtual vm_external * ts_clone() { return new vm_rb_map(m_map); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_rb_map))) vm_rb_map(m_map); }
+    virtual vm_external * ts_clone() override { return new vm_rb_map(m_map); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_rb_map))) vm_rb_map(m_map); }
 };
 
 vm_obj_map const & to_map(vm_obj const & o) {
diff --git a/src/library/vm/vm_task.cpp b/src/library/vm/vm_task.cpp
index 5c06ab925f..29f1dd0dfa 100644
--- a/src/library/vm/vm_task.cpp
+++ b/src/library/vm/vm_task.cpp
@@ -49,8 +49,8 @@ struct vm_task : public vm_external {
     vm_task(task_result<vm_obj> const & v) : m_val(v) {}
     virtual ~vm_task() {}
     virtual void dealloc() override { this->~vm_task(); get_vm_allocator().deallocate(sizeof(vm_task), this); }
-    virtual vm_external * ts_clone() { return new vm_task(m_val); }
-    virtual vm_external * clone() { return new (get_vm_allocator().allocate(sizeof(vm_task))) vm_task(m_val); }
+    virtual vm_external * ts_clone() override { return new vm_task(m_val); }
+    virtual vm_external * clone() override { return new (get_vm_allocator().allocate(sizeof(vm_task))) vm_task(m_val); }
 };
 
 bool is_task(vm_obj const & o) {