diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 727832d70..2bacb3a4f 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -194,7 +194,6 @@ class mbp::impl {
 
 
     void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) {
-        ast_manager& m = vars.get_manager();
         expr_mark lit_visited;
         project_plugin::mark_rec(lit_visited, lits);
 
diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index ef6b0e776..5e0539787 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -75,7 +75,7 @@ namespace smt {
         ast_manager& m = get_manager();
         context& ctx = get_context();
         theory_var r  = theory_array_base::mk_var(n);
-        VERIFY(r == m_find.mk_var());
+        VERIFY(r == static_cast<theory_var>(m_find.mk_var()));
         SASSERT(r == static_cast<int>(m_var_data.size()));
         m_var_data.push_back(alloc(var_data));
         var_data * d  = m_var_data[r];
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index e5c8b1313..8e140661b 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -198,7 +198,7 @@ namespace smt {
 
     theory_var theory_datatype::mk_var(enode * n) {
         theory_var r  = theory::mk_var(n);
-        VERIFY(r == m_find.mk_var());
+        VERIFY(r == static_cast<theory_var>(m_find.mk_var()));
         SASSERT(r == static_cast<int>(m_var_data.size()));
         m_var_data.push_back(alloc(var_data));
         var_data * d  = m_var_data[r];
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 23095f03a..f2145c85b 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -88,8 +88,6 @@ namespace smt {
     }
 
     expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_max_unspecified(func_decl * f, expr * x, expr * y) {
-        unsigned ebits = m_util.get_ebits(f->get_range());
-        unsigned sbits = m_util.get_sbits(f->get_range());
 
         expr_ref a(m), wrapped(m), wu(m), wu_eq(m);
         a = m.mk_app(f, x, y);