diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 626348ee8..051ae98a7 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -39,8 +39,8 @@ namespace sls {
         m_ld(*this),
         m_repair_down(m.get_num_asts(), m_gd),
         m_repair_up(m.get_num_asts(), m_ld),
-        m_todo(m),
-        m_constraint_trail(m) {
+        m_constraint_trail(m),
+        m_todo(m) {
     }
 
     void context::updt_params(params_ref const& p) {
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index aea9e55ac..f5aba0083 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -182,7 +182,6 @@ namespace sls {
 
     void datatype_plugin::add_axioms() {
         expr_ref_vector axioms(m);
-        expr* u = nullptr;
         for (auto t : ctx.subterms()) {
             auto s = t->get_sort();
             if (dt.is_datatype(s)) 
diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h
index a28dd65c0..f06e24963 100644
--- a/src/ast/sls/sls_datatype_plugin.h
+++ b/src/ast/sls/sls_datatype_plugin.h
@@ -82,7 +82,7 @@ namespace sls {
     public:
         datatype_plugin(context& c);
         ~datatype_plugin() override;
-        family_id fid() { return m_fid; }
+        family_id fid() override { return m_fid; }
         expr_ref get_value(expr* e) override;
         void initialize() override;
         void start_propagation() override;
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index e4e9f1200..09efea199 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -78,7 +78,7 @@ namespace sls {
             m_context.register_atom(v, e);
         }
 
-        std::ostream& display(std::ostream& out) {
+        std::ostream& display(std::ostream& out) override {
             m_ddfw.display(out);
             m_context.display(out);
             return out;