diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 959ce6f14..6af48b823 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -565,7 +565,6 @@ namespace smt {
 
     // start exploring subgraph below `app`
     bool theory_datatype::occurs_check_enter(enode * app) {
-        context& ctx = get_context();
         app = app->get_root();
         theory_var v = app->get_th_var(get_id());
         if (v == null_theory_var) {
@@ -759,7 +758,6 @@ namespace smt {
         SASSERT(d->m_constructor);
         func_decl * c_decl = d->m_constructor->get_decl();
         datatype_value_proc * result = alloc(datatype_value_proc, c_decl);
-        unsigned num = d->m_constructor->get_num_args();
         for (enode* arg : enode::args(d->m_constructor)) {
             result->add_dependency(arg);
         }
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 62058e0e9..33b66639b 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -860,7 +860,6 @@ namespace smtfd {
            Enforce M[x] == rewrite(M[x]) for every A[x] such that M = A under current model.
          */
         void beta_reduce(expr* t) {
-            bool added = false;
             if (m_autil.is_map(t) ||
                 m_autil.is_const(t) ||
                 is_lambda(t)) {