diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 80af80266..829aa0103 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -697,8 +697,6 @@ namespace datalog {
             strats_index++;
         }
         //we have managed to topologicaly order all the components
-        SASSERT(std::find_if(m_components.begin(), m_components.end(),
-            std::bind1st(std::not_equal_to<item_set*>(), (item_set*)0)) == m_components.end());
 
         //reverse the strats array, so that the only the later components would depend on earlier ones
         std::reverse(m_strats.begin(), m_strats.end());
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index df2491a3e..39bcb0e02 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3291,7 +3291,6 @@ namespace smt {
               for (app* n : m_underspecified_ops) {
                   tout << mk_pp(n, get_manager()) << "\n";
               });
-        context& ctx = get_context();
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
         compute_epsilon();
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index ecd6aae44..c8689900b 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -928,14 +928,12 @@ namespace smtfd {
             expr_ref_vector eqs(m);
             m_args.reset();
             m_args.push_back(a);
-            bool all_eq = true;
             for (unsigned i = 1; i < t->get_num_args(); ++i) {
                 expr* arg1 = t->get_arg(i);
                 expr* arg2 = store->get_arg(i);
                 if (arg1 == arg2) continue;
                 expr_ref v1 = eval_abs(arg1);
                 expr_ref v2 = eval_abs(arg2);
-                if (v1 != v2) all_eq = false;
                 m_args.push_back(arg1);
                 eqs.push_back(m.mk_eq(arg1, arg2));
             }