diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index b134d38cb..6780145d9 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1662,7 +1662,7 @@ ast * ast_manager::register_node_core(ast * n) {
             for (unsigned i = 0; i < num_args; i++) {
                 expr * arg = t->get_arg(i);
                 inc_ref(arg);
-                unsigned arg_depth;
+                unsigned arg_depth = 0;
                 switch (arg->get_kind()) {
                 case AST_APP: {
                     app_flags * arg_flags = to_app(arg)->flags();
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 8cf158604..bd2676ee4 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -252,7 +252,7 @@ func_decl * fpa_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_paramete
 
 func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                                    unsigned arity, sort * const * domain, sort * range) {
-    sort * s;
+    sort * s = 0;
     if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) {
         s = to_sort(parameters[0].get_ast());
     }
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 291712805..6aee683ff 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -724,8 +724,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
         scoped_mpq q(m_fm.mpq_manager());        
         m_fm.to_sbv_mpq(rmv, v, q);
         
-        rational r(q);
-        unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
+        rational r(q);        
         rational ul, ll;
         ul = m_fm.m_powers2.m1(bv_sz);
         ll = rational(0);
@@ -758,8 +757,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
         scoped_mpq q(m_fm.mpq_manager());
         m_fm.to_sbv_mpq(rmv, v, q);
         
-        rational r(q);
-        unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
+        rational r(q);        
         rational ul, ll;
         ul = m_fm.m_powers2.m1(bv_sz - 1);
         ll = - m_fm.m_powers2(bv_sz - 1);
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 50466c276..4b87f9e65 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -700,7 +700,7 @@ namespace nlsat {
         void add_root_literal(atom::kind k, var y, unsigned i, poly * p) {
             scoped_mpz c(m_pm.m());
             bool_var b;
-            bool     lsign;
+            bool     lsign = false;
             if (m_pm.degree(p, y) == 1 && m_pm.const_coeff(p, y, 1, c)) {
                 SASSERT(!m_pm.m().is_zero(c));
                 // literal can be expressed using a linear ineq_atom