diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index ad7fd73d5..508d551ee 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -74,8 +74,6 @@ namespace sls {
         svector<bool> m_sls_phase;
         svector<double> m_rewards;
         svector<sat::bool_var> m_smt_bool_var2sls_bool_var, m_sls_bool_var2smt_bool_var;
-
-
         
         bool is_shared(sat::literal lit);
         void run();
@@ -155,7 +153,5 @@ namespace sls {
             m_new_clause_added = true;
         }
         void force_restart() override { m_ddfw->force_restart(); }
-
-
     };
 }
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
index 003456edd..429e79425 100644
--- a/src/smt/theory_sls.h
+++ b/src/smt/theory_sls.h
@@ -48,7 +48,6 @@ namespace sls {
 
 
 namespace smt {
-    class context;
 
     class theory_sls : public smt::theory, public sls::smt_context {
         model_ref m_model;
@@ -63,6 +62,8 @@ namespace smt {
         theory_sls(context& ctx);
         ~theory_sls() override;
         model_ref get_model() { return m_model; }
+
+        // smt::theory interface
         char const* get_name() const override { return "sls"; }
         void init() override;
         void pop_scope_eh(unsigned n) override;
@@ -75,6 +76,7 @@ namespace smt {
         void new_eq_eh(theory_var v1, theory_var v2) override {}
         void new_diseq_eh(theory_var v1, theory_var v2) override {}
 
+        // sls::smt_context interface
         ast_manager& get_manager() override { return m; }
         params_ref get_params() override;
         void initialize_value(expr* t, expr* v) override;
@@ -84,7 +86,6 @@ namespace smt {
         expr* bool_var2expr(sat::bool_var v) override;
         void set_finished() override;
         unsigned get_num_bool_vars() const override;
-
     };
 
 }