diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index bbf639df4..6e9a71245 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3215,7 +3215,6 @@ bool theory_seq::branch_nqs() {
 }
 
 void theory_seq::branch_nq(ne const& n) {
-    context& ctx = get_context();
     literal eq = mk_eq(n.l(), n.r(), false);
     literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
     literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 8f7dad423..b0e61db88 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -385,7 +385,6 @@ namespace smtfd {
             m_lemmas(m), 
             m_rewriter(m)
         {
-            (void)m;
         }
 
         void set_max_lemmas(unsigned max) {            
@@ -398,7 +397,7 @@ namespace smtfd {
 
         void add(expr* f, char const* msg) { m_lemmas.push_back(f); TRACE("smtfd", tout << msg << " " << mk_bounded_pp(f, m, 2) << "\n";); }
 
-        ast_manager& get_manager() { return m_lemmas.get_manager(); }
+        ast_manager& get_manager() { return m; }
 
         bool at_max() const { return m_lemmas.size() >= m_max_lemmas; }