diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3dff97875..47a456b24 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 
+#include <cmath>
 #include "sat/sat_solver.h"
 #include "sat/sat_integrity_checker.h"
 #include "sat/sat_lookahead.h"
diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp
index 127b6f5a0..cab5ef0c5 100644
--- a/src/tactic/model_converter.cpp
+++ b/src/tactic/model_converter.cpp
@@ -120,7 +120,7 @@ public:
         m = m_model;
     }
 
-    void operator()(labels_vec & r) {
+    void operator()(labels_vec & r) override {
         r.append(m_labels.size(), m_labels.c_ptr());
     }
 
diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp
index 7099f0fdf..f2f7e00c8 100644
--- a/src/tactic/sine_filter.cpp
+++ b/src/tactic/sine_filter.cpp
@@ -36,14 +36,14 @@ public:
     sine_tactic(ast_manager& m, params_ref const& p): 
         m(m), m_params(p) {}
     
-    virtual tactic * translate(ast_manager & m) {
+    tactic * translate(ast_manager & m) override {
         return alloc(sine_tactic, m, m_params);
     }
 
-    virtual void updt_params(params_ref const & p) {
+    void updt_params(params_ref const & p) override {
     }
 
-    virtual void collect_param_descrs(param_descrs & r) {
+    void collect_param_descrs(param_descrs & r) override {
     }
 
     void operator()(goal_ref const & g, goal_ref_buffer& result) override {
@@ -63,7 +63,7 @@ public:
         SASSERT(g->is_well_sorted());
     }
     
-    virtual void cleanup() {
+    void cleanup() override {
     }
 
 private:
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 1899876df..738a3b367 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -1040,7 +1040,7 @@ public:
     
     virtual ~fail_if_tactic() {}
 
-    void cleanup() {}
+    void cleanup() override {}
 
     void  operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (m_p->operator()(*(in.get())).is_true()) {
@@ -1093,7 +1093,7 @@ public:
         }
     }
 
-    virtual tactic * translate(ast_manager & m) { return translate_core<if_no_unsat_cores_tactical>(m); }
+    tactic * translate(ast_manager & m) override { return translate_core<if_no_unsat_cores_tactical>(m); }
 };
 
 class if_no_models_tactical : public unary_tactical {
@@ -1109,7 +1109,9 @@ public:
         }
     }
 
-    virtual tactic * translate(ast_manager & m) { return translate_core<if_no_models_tactical>(m); }
+    tactic * translate(ast_manager & m) override { 
+        return translate_core<if_no_models_tactical>(m); 
+    }
 };
 
 tactic * if_no_proofs(tactic * t) {