diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index f5dc20260..ecc48fdca 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -2240,12 +2240,12 @@ namespace sls {
             return value(v) == abs(value(od.m_arg1));
         }
         case arith_op_kind::OP_TO_INT: {
-            auto od = m_ops[vi.m_def_idx];
+            // auto od = m_ops[vi.m_def_idx];
             NOT_IMPLEMENTED_YET();
             break;
         }
         case arith_op_kind::OP_TO_REAL: {
-            auto od = m_ops[vi.m_def_idx];
+            // auto od = m_ops[vi.m_def_idx];
             NOT_IMPLEMENTED_YET();
             break;
         }
diff --git a/src/ast/sls/sls_basic_plugin.h b/src/ast/sls/sls_basic_plugin.h
index 63ac3ed5d..6c1936532 100644
--- a/src/ast/sls/sls_basic_plugin.h
+++ b/src/ast/sls/sls_basic_plugin.h
@@ -17,7 +17,6 @@ Author:
 namespace sls {
 
     class basic_plugin : public plugin {
-        bool               m_initialized = false;
         expr_mark          m_axiomatized;
         
         bool is_basic(expr* e) const;
diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp
index 5b9d064bb..9004128b9 100644
--- a/src/ast/sls/sls_bv_terms.cpp
+++ b/src/ast/sls/sls_bv_terms.cpp
@@ -23,7 +23,6 @@ Author:
 namespace sls {
 
     bv_terms::bv_terms(sls::context& ctx):
-        ctx(ctx),
         m(ctx.get_manager()), 
         bv(m),
         m_axioms(m) {}
diff --git a/src/ast/sls/sls_bv_terms.h b/src/ast/sls/sls_bv_terms.h
index 98d57dead..effd74eeb 100644
--- a/src/ast/sls/sls_bv_terms.h
+++ b/src/ast/sls/sls_bv_terms.h
@@ -29,7 +29,6 @@ Author:
 namespace sls {
 
     class bv_terms {
-        sls::context&       ctx;
         ast_manager&        m;
         bv_util             bv;
         expr_ref_vector     m_axioms;
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index f5aba0083..d4789d006 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -430,7 +430,6 @@ namespace sls {
     }
 
     euf::enode* datatype_plugin::get_constructor(euf::enode* n) const {
-        euf::enode* con = nullptr;
         for (auto sib : euf::enode_class(n))
             if (dt.is_constructor(sib->get_expr()))
                 return sib;
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index e7263fafc..48ab3cb96 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -101,7 +101,6 @@ namespace sls {
         g.explain<size_t>(explain, nullptr);
         g.end_explain();
         double reward = -1;
-        bool has_flipped = false;
         TRACE("enf",
             for (auto p : explain) {
                 sat::literal l = to_literal(p);
diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h
index 6bd0dfcb2..a9e5032d2 100644
--- a/src/ast/sls/sls_euf_plugin.h
+++ b/src/ast/sls/sls_euf_plugin.h
@@ -70,7 +70,6 @@ namespace sls {
     public:
         euf_plugin(context& c);
         ~euf_plugin() override;
-        family_id fid() { 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_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
index 6f0a342cc..2b704fa3f 100644
--- a/src/ast/sls/sls_smt_plugin.cpp
+++ b/src/ast/sls/sls_smt_plugin.cpp
@@ -64,7 +64,7 @@ namespace sls {
                 continue;
             m_context.register_atom(v, m_smt2sls_tr(e));
             for (auto t : subterms::all(expr_ref(e, m)))
-                add_shared_term(e);
+                add_shared_term(t);
         }
 
         for (auto fml : fmls) 
@@ -82,7 +82,7 @@ namespace sls {
                 continue;
             add_shared_var(v, w); 
             for (auto t : subterms::all(expr_ref(e, m)))
-                add_shared_term(e);
+                add_shared_term(t);
         }
 
         m_thread = std::thread([this]() { run(); });