diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 2b2087e3b..258c28369 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -985,7 +985,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
 
 br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
     numeral a;
-    expr* x;
+    expr* x = 0;
     if (m_util.is_numeral(arg, a)) {
         result = m_util.mk_numeral(floor(a), true);
         return BR_DONE;
diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index e9b383b56..229db4d27 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -668,7 +668,7 @@ namespace datalog {
             T * el = it->m_key;
             item_set * out_edges = it->m_value;
 
-            unsigned el_comp;
+            unsigned el_comp = 0;
             VERIFY( m_component_nums.find(el, el_comp) );
 
             item_set::iterator eit = out_edges->begin();
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 74206a1f6..9e02a764f 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -294,7 +294,7 @@ namespace datalog {
     }
 
     table_relation_plugin & relation_manager::get_table_relation_plugin(table_plugin & tp) {
-        table_relation_plugin * res;
+        table_relation_plugin * res = 0;
         VERIFY( m_table_relation_plugins.find(&tp, res) );
         return *res;
     }
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 58d319a63..15b723c8c 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -216,7 +216,7 @@ namespace opt {
         rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector<expr>& keys, vector<rational>& weights) {
             rational min_weight(-1);
             for (unsigned i = 0; i < core.size(); ++i) {
-                expr* e;
+                expr* e = 0;
                 VERIFY(m.is_not(core[i], e));
                 keys.push_back(m_keys[e]);
                 rational weight = m_weights[e];
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 4281ec909..d8ae75256 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -2503,7 +2503,7 @@ public:
         }
         
         virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
-            nlarith::branch_conditions *brs;
+            nlarith::branch_conditions *brs = 0;
             VERIFY (m_cache.find(x.x(), fml, brs));
             SASSERT(vl.is_unsigned());
             SASSERT(vl.get_unsigned() < brs->size());
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 65272207e..20813602e 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -103,6 +103,7 @@ namespace smt {
 
     void context::justify(literal lit, index_set& s) {
         ast_manager& m = m_manager;
+        (void)m;
         b_justification js = get_justification(lit.var());
         switch (js.get_kind()) {
         case b_justification::CLAUSE: {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 76e721faa..2bd4844e8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -765,7 +765,7 @@ namespace smt {
         }
         
         void internalize_eq_eh(app * atom, bool_var) {
-            expr* lhs, *rhs;
+            expr* lhs = 0, *rhs = 0;
             VERIFY(m.is_eq(atom, lhs, rhs));
             enode * n1 = get_enode(lhs);
             enode * n2 = get_enode(rhs);
@@ -892,7 +892,7 @@ namespace smt {
         // to_int (to_real x) = x
         // to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
         void mk_to_int_axiom(app* n) {
-            expr* x, *y;
+            expr* x = 0, *y = 0;
             VERIFY (a.is_to_int(n, x));            
             if (a.is_to_real(x, y)) {
                 mk_axiom(th.mk_eq(y, n, false));
@@ -908,7 +908,7 @@ namespace smt {
 
         // is_int(x) <=> to_real(to_int(x)) = x
         void mk_is_int_axiom(app* n) {
-            expr* x;
+            expr* x = 0;
             VERIFY(a.is_is_int(n, x));
             literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
             literal is_int = ctx().get_literal(n);
@@ -1299,12 +1299,14 @@ namespace smt {
                 return;
             }
             int num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
+            (void)num_of_p;
             local_bound_propagator bp(*this);
             m_solver->propagate_bounds_for_touched_rows(bp);
             if (m.canceled()) {
                 return;
             }
             int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
+            (void)new_num_of_p;
             CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
             if (m_solver->get_status() == lean::lp_status::INFEASIBLE) {
                 set_conflict();
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index ea53f1342..dfb535f51 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1074,7 +1074,7 @@ expr_ref theory_seq::mk_first(expr* s) {
 
 
 void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     zstring s;
     if (m_util.str.is_empty(e)) {
         head = m_util.str.mk_unit(mk_nth(e, m_autil.mk_int(0)));
@@ -1401,7 +1401,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
      // true if a occurs under an interpreted function or under left/right selector.
     SASSERT(is_var(a));
     SASSERT(m_todo.empty());
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     m_todo.push_back(b);
     while (!m_todo.empty()) {
         b = m_todo.back();
@@ -1990,7 +1990,7 @@ bool theory_seq::solve_nc(unsigned idx) {
         return true;
     }
 
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     if (m.is_eq(c, e1, e2)) {
         literal eq = mk_eq(e1, e2, false);
         propagate_lit(deps, 0, 0, ~eq);
@@ -2316,7 +2316,7 @@ bool theory_seq::check_int_string() {
 
 bool theory_seq::add_stoi_axiom(expr* e) {
     context& ctx = get_context();
-    expr* n;
+    expr* n = 0;
     rational val;
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
     VERIFY(m_util.str.is_stoi(e, n));    
@@ -2398,7 +2398,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
 bool theory_seq::add_itos_axiom(expr* e) {
     context& ctx = get_context();
     rational val;
-    expr* n;
+    expr* n = 0;
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
     VERIFY(m_util.str.is_itos(e, n));
     if (get_num_value(n, val)) {
@@ -3197,7 +3197,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
 
 */
 void theory_seq::add_replace_axiom(expr* r) {
-    expr* a, *s, *t;
+    expr* a = 0, *s = 0, *t = 0;
     VERIFY(m_util.str.is_replace(r, a, s, t));
     expr_ref x  = mk_skolem(m_indexof_left, a, s);
     expr_ref y  = mk_skolem(m_indexof_right, a, s);
@@ -3330,7 +3330,7 @@ void theory_seq::add_itos_length_axiom(expr* len) {
 
 void theory_seq::propagate_in_re(expr* n, bool is_true) {
     TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";);
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     VERIFY(m_util.str.is_in_re(n, e1, e2));
 
     expr_ref tmp(n, m);
@@ -3462,7 +3462,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
     if (!tha) return false;
     rational val1;
     expr_ref len(m), len_val(m);
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     ptr_vector<expr> todo;
     todo.push_back(e);
     val.reset();
@@ -3522,7 +3522,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
 */
 
 void theory_seq::add_extract_axiom(expr* e) {
-    expr* s, *i, *l;
+    expr* s = 0, *i = 0, *l = 0;
     VERIFY(m_util.str.is_extract(e, s, i, l));
     if (is_tail(s, i, l)) {
         add_tail_axiom(e, s);
@@ -3682,7 +3682,7 @@ void theory_seq::add_at_axiom(expr* e) {
 */
 void theory_seq::propagate_step(literal lit, expr* step) {
     SASSERT(get_context().get_assignment(lit) == l_true);
-    expr* re, *acc, *s, *idx, *i, *j;
+    expr* re = 0, *acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0;
     VERIFY(is_step(step, s, idx, re, i, j, acc));
     TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";);
     propagate_lit(0, 1, &lit, mk_literal(acc));
@@ -3843,7 +3843,7 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
 void theory_seq::assign_eh(bool_var v, bool is_true) {
     context & ctx = get_context();
     expr* e = ctx.bool_var2expr(v);
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     expr_ref f(m);
     bool change = false;
     literal lit(v, !is_true);
@@ -4191,7 +4191,7 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned
    rej(s, idx, re, i) -> len(s) > idx     if i is final
 */
 void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
-    expr *s, * idx, *re;
+    expr *s = 0, *idx = 0, *re = 0;
     unsigned src;
     eautomaton* aut = 0;
     bool is_acc;
@@ -4220,7 +4220,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) {
 
     TRACE("seq", tout << mk_pp(acc, m) << "\n";);
     SASSERT(ctx.get_assignment(acc) == l_true);
-    expr *e, * idx, *re;
+    expr *e = 0, *idx = 0, *re = 0;
     expr_ref step(m);
     unsigned src;
     eautomaton* aut = 0;
@@ -4299,7 +4299,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) {
 bool theory_seq::add_step2accept(expr* step, bool& change) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(step) == l_true);
-    expr* re, *_acc, *s, *idx, *i, *j;
+    expr* re = 0, *_acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0;
     VERIFY(is_step(step, s, idx, re, i, j, _acc));
     literal acc1 = mk_accept(s, idx,  re, i);
     switch (ctx.get_assignment(acc1)) {
@@ -4348,7 +4348,7 @@ Recall we also have:
 bool theory_seq::add_reject2reject(expr* rej, bool& change) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(rej) == l_true);
-    expr* s, *idx, *re;
+    expr* s = 0, *idx = 0, *re = 0;
     unsigned src;
     rational r;
     eautomaton* aut = 0;
@@ -4410,7 +4410,7 @@ bool theory_seq::add_reject2reject(expr* rej, bool& change) {
 
 void theory_seq::propagate_not_prefix(expr* e) {
     context& ctx = get_context();
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     VERIFY(m_util.str.is_prefix(e, e1, e2));
     literal lit = ctx.get_literal(e);
     SASSERT(ctx.get_assignment(lit) == l_false);
@@ -4439,7 +4439,7 @@ void theory_seq::propagate_not_prefix(expr* e) {
 
 void theory_seq::propagate_not_prefix2(expr* e) {
     context& ctx = get_context();
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     VERIFY(m_util.str.is_prefix(e, e1, e2));
     literal lit = ctx.get_literal(e);
     SASSERT(ctx.get_assignment(lit) == l_false);
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 83693abba..e293ade17 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -168,7 +168,7 @@ public:
 
         // translate bit-vector consequences back to integer values
         for (unsigned i = 0; i < consequences.size(); ++i) {
-            expr* a, *b, *u, *v;
+            expr* a = 0, *b = 0, *u = 0, *v = 0;
             func_decl* f;
             rational num;
             unsigned bvsize;
@@ -228,7 +228,7 @@ private:
         for (; it != end; ++it) {
             expr* e = *it;
             rational lo, hi;
-            bool s1, s2;
+            bool s1 = false, s2 = false;
             SASSERT(is_uninterp_const(e));
             func_decl* f = to_app(e)->get_decl();
 
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 35601f374..8c9ff122d 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -116,7 +116,7 @@ public:
 
         // translate enumeration constants to bit-vectors.
         for (unsigned i = 0; i < vars.size(); ++i) {
-            func_decl* f;
+            func_decl* f = 0;
             if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {
                 bvars.push_back(m.mk_const(f));
             }
@@ -128,7 +128,7 @@ public:
 
         // translate bit-vector consequences back to enumeration types
         for (unsigned i = 0; i < consequences.size(); ++i) {
-            expr* a, *b, *u, *v;
+            expr* a = 0, *b = 0, *u = 0, *v = 0;
             func_decl* f;
             rational num;
             unsigned bvsize;