diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 7ebc0766e..383c63b8f 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -24,28 +24,28 @@ namespace sls {
     bool arith_base<num_t>::ineq::is_true() const {
         switch (m_op) {
         case ineq_kind::LE:
-            return m_args_value + m_coeff <= 0;
+            return m_args_value + this->m_coeff <= 0;
         case ineq_kind::EQ:
-            return m_args_value + m_coeff == 0;
+            return m_args_value + this->m_coeff == 0;
         default:
-            return m_args_value + m_coeff < 0;
+            return m_args_value + this->m_coeff < 0;
         }
     }
 
     template<typename num_t>
     std::ostream& arith_base<num_t>::ineq::display(std::ostream& out) const {
         bool first = true;
-        for (auto const& [c, v] : m_args)
+        for (auto const& [c, v] : this->m_args)
             out << (first ? "" : " + ") << c << " * v" << v, first = false;
-        if (m_coeff != 0)
-            out << " + " << m_coeff;
+        if (this->m_coeff != 0)
+            out << " + " << this->m_coeff;
         switch (m_op) {
         case ineq_kind::LE:
-            return out << " <= " << 0 << "(" << m_args_value + m_coeff << ")";
+            return out << " <= " << 0 << "(" << m_args_value + this->m_coeff << ")";
         case ineq_kind::EQ:
-            return out << " == " << 0 << "(" << m_args_value + m_coeff << ")";
+            return out << " == " << 0 << "(" << m_args_value + this->m_coeff << ")";
         default:
-            return out << " < " << 0 << "(" << m_args_value + m_coeff << ")";
+            return out << " < " << 0 << "(" << m_args_value + this->m_coeff << ")";
         }
     }    
 
@@ -486,7 +486,7 @@ namespace sls {
     typename arith_base<num_t>::var_t arith_base<num_t>::mk_op(arith_op_kind k, expr* e, expr* x, expr* y) {
         auto v = mk_var(e);
         auto w = mk_term(x);
-        auto u = mk_term(y);
+	//        auto u = mk_term(y);
         unsigned idx = m_ops.size();
         num_t val;
         switch (k) {
@@ -533,7 +533,7 @@ namespace sls {
         v = mk_var(e);
         auto idx = m_adds.size();
         num_t sum(t.m_coeff);
-        m_adds.push_back({ t.m_args, t.m_coeff, v });
+        m_adds.push_back({ { t.m_args, t.m_coeff }, v });
         for (auto const& [c, w] : t.m_args)
             m_vars[w].m_adds.push_back(idx), sum += c * value(w);
         m_vars[v].m_def_idx = idx;
@@ -829,7 +829,6 @@ namespace sls {
 
     template<typename num_t>
     void arith_base<num_t>::repair_rem(op_def const& od) {
-        auto val = value(od.m_var);
         auto v1 = value(od.m_arg1);
         auto v2 = value(od.m_arg2);
         if (v2 == 0) {
@@ -874,7 +873,6 @@ namespace sls {
 
     template<typename num_t>
     void arith_base<num_t>::repair_power(op_def const& od) {
-        auto val = value(od.m_var);
         auto v1 = value(od.m_arg1);
         auto v2 = value(od.m_arg2);
         if (v1 == 0 && v2 == 0) {
@@ -916,7 +914,6 @@ namespace sls {
 
     template<typename num_t>
     void arith_base<num_t>::repair_idiv(op_def const& od) {
-        auto val = value(od.m_var);
         auto v1 = value(od.m_arg1);
         auto v2 = value(od.m_arg2);
         IF_VERBOSE(0, verbose_stream() << "todo repair div");
@@ -926,7 +923,6 @@ namespace sls {
     
     template<typename num_t>
     void arith_base<num_t>::repair_div(op_def const& od) {
-        auto val = value(od.m_var);
         auto v1 = value(od.m_arg1);
         auto v2 = value(od.m_arg2);
         IF_VERBOSE(0, verbose_stream() << "todo repair /");
@@ -954,7 +950,7 @@ namespace sls {
             if (!cm(*ineq, x, coeff, new_value))
                 continue;
             double result = 0;
-            auto old_value = m_vars[x].m_value;
+	    //            auto old_value = m_vars[x].m_value;
             for (auto const& [coeff, bv] : m_vars[x].m_bool_vars) {
                 result += ctx.reward(bv);
 #if 0
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index d24d7697f..3d91255d7 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -56,6 +56,7 @@ namespace sls {
 
     class sat_solver_context {
     public:
+        virtual ~sat_solver_context() {}
         virtual vector<sat::clause_info> const& clauses() const = 0;
         virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
         virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index 0de1fbe42..bd79245e8 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -15,7 +15,6 @@ Author:
     
 --*/
 
-#pragma once
 #include "ast/sls/sls_context.h"
 #include "ast/sls/sat_ddfw.h"
 #include "ast/sls/sls_smt_solver.h"
diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp
index 3f244e233..e079e72cc 100644
--- a/src/sat/smt/sls_solver.cpp
+++ b/src/sat/smt/sls_solver.cpp
@@ -68,14 +68,13 @@ namespace sls {
     }       
 
     class solver::smt_plugin : public sat::local_search_plugin, public sls::sat_solver_context {
-        ast_manager& m;
-        sat::ddfw* m_ddfw;
         solver& s;
+        sat::ddfw* m_ddfw;
         sls::context m_context;
         bool m_new_clause_added = false;
     public:
         smt_plugin(ast_manager& m, solver& s, sat::ddfw* d) : 
-            m(m), s(s), m_ddfw(d), m_context(m, *this) {}
+	    s(s), m_ddfw(d), m_context(m, *this) {}
 
         void init_search() override {}
 
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index b7345fc68..6310c0dd1 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -110,7 +110,6 @@ static void track_clauses(sat::solver const& src,
         dst.mk_var(false, true);
     }
     sat::literal_vector lits;
-    sat::literal lit;
     sat::clause * const * it  = src.begin_clauses();
     sat::clause * const * end = src.end_clauses();
     svector<sat::solver::bin_clause> bin_clauses;