diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index 13416c086..46f610c18 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -324,7 +324,7 @@ namespace datalog {
         if (!is_rel_sort(r, sorts)) {
             return 0;
         }
-        unsigned index0;
+        unsigned index0 = 0;
         sort* last_sort = 0;
         SASSERT(num_params > 0);
         for (unsigned i = 0; i < num_params; ++i) {
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index d833e2381..e89664216 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2267,6 +2267,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
 
         expr * bv = args[0];
         int sz = m_bv_util.get_bv_size(bv);
+        (void)to_sbits;
         SASSERT((unsigned)sz == to_sbits + to_ebits);
 
         result = m_util.mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
@@ -2399,6 +2400,7 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
 
         res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
         unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
+        (void) sig_sz;
         SASSERT(sig_sz == to_sbits + 4);
 
         expr_ref exponent_overflow(m), exponent_underflow(m);
diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp
index 16e9098fc..c1d9b36a5 100644
--- a/src/ast/normal_forms/defined_names.cpp
+++ b/src/ast/normal_forms/defined_names.cpp
@@ -210,7 +210,7 @@ bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_
         TRACE("mk_definition_bug", tout << "name for expression is already cached..., returning false...\n";);        
         n = n_ptr;
         if (m_manager.proofs_enabled()) {
-            proof * pr_ptr;
+            proof * pr_ptr = 0;
             m_expr2proof.find(e, pr_ptr);
             SASSERT(pr_ptr);
             pr = pr_ptr;
diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp
index 5158439a7..bb9b30dc5 100644
--- a/src/ast/normal_forms/pull_quant.cpp
+++ b/src/ast/normal_forms/pull_quant.cpp
@@ -58,7 +58,7 @@ struct pull_quant::imp {
             }
             
             bool found_quantifier = false;
-            bool forall_children;
+            bool forall_children = false;
             
             for (unsigned i = 0; i < num_children; i++) {
                 expr * child = children[i];
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 71be3d1c2..66c5e66bc 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -572,7 +572,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
 
 */
 br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
-    expr* cond, *t, *e;
+    expr* cond = 0, *t = 0, *e = 0;
     VERIFY(m().is_ite(ite, cond, t, e));
     SASSERT(m().is_value(val));
 
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index eaf5713ee..9c200a3e2 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -103,8 +103,8 @@ template<typename Config>
 template<bool ProofGen>
 bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";);
-    expr *  new_t;
-    proof * new_t_pr;
+    expr *  new_t = 0;
+    proof * new_t_pr = 0;
     if (m_cfg.get_subst(t, new_t, new_t_pr)) {
         TRACE("rewriter_subst", tout << "subst\n" << mk_ismt2_pp(t, m()) << "\n---->\n" << mk_ismt2_pp(new_t, m()) << "\n";);
         SASSERT(m().get_sort(t) == m().get_sort(new_t));
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 04acd7ee1..29bfe25e5 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -303,7 +303,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
     }
     else if (u.re.is_full(e)) {
         expr_ref tt(m.mk_true(), m);
-        sort* seq_s, *char_s;
+        sort *seq_s = 0, *char_s = 0;
         VERIFY (u.is_re(m.get_sort(e), seq_s));
         VERIFY (u.is_seq(seq_s, char_s));
         sym_expr* _true = sym_expr::mk_pred(tt, char_s);
@@ -794,7 +794,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
 
     bool isc1 = false;
     bool isc2 = false;
-    expr* a1, *a2, *b1, *b2;
+    expr *a1 = 0, *a2 = 0, *b1 = 0, *b2 = 0;
     if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
         isc1 = true;
     }
@@ -1321,7 +1321,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
 }
 
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
-    sort* s;
+    sort* s = 0;
     VERIFY(m_util.is_re(a, s));
     result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a);
     return BR_REWRITE1;
diff --git a/src/ast/simplifier/bit2int.cpp b/src/ast/simplifier/bit2int.cpp
index ab4193486..08c3da774 100644
--- a/src/ast/simplifier/bit2int.cpp
+++ b/src/ast/simplifier/bit2int.cpp
@@ -273,7 +273,7 @@ void bit2int::visit(app* n) {
     // bv2int(x) <= z - bv2int(y) -> bv2int(x) + bv2int(y) <= z
     //
     
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     expr_ref tmp1(m_manager), tmp2(m_manager);
     expr_ref tmp3(m_manager);
     expr_ref pos1(m_manager), neg1(m_manager);
diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp
index be293c5a8..eea1938a6 100644
--- a/src/ast/substitution/substitution.cpp
+++ b/src/ast/substitution/substitution.cpp
@@ -146,7 +146,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
                 bool has_new_args = false;
                 for (unsigned i = 0; i < num_args; i++) {
                     expr * arg     = to_app(e)->get_arg(i);
-                    expr * new_arg;
+                    expr * new_arg = 0;
                     
                     VERIFY(m_apply_cache.find(expr_offset(arg, off), new_arg));
                     new_args.push_back(new_arg);
diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h
index ab55a44c3..e288bb076 100644
--- a/src/math/hilbert/heap_trie.h
+++ b/src/math/hilbert/heap_trie.h
@@ -283,7 +283,7 @@ public:
         ++m_stats.m_num_removes;
         // assumption: key is in table.
         node* n = m_root;
-        node* m;
+        node* m = 0;
         for (unsigned i = 0; i < num_keys(); ++i) {
             n->dec_ref();
             VERIFY (to_trie(n)->find(get_key(keys, i), m));
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index f4eb8a003..986c17664 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -1035,7 +1035,7 @@ namespace algebraic_numbers {
 
                 unsigned num_rem  = 0; // number of remaining sequences
                 unsigned target_i = UINT_MAX; // index of sequence that is isolating
-                int target_lV, target_uV;
+                int target_lV = 0, target_uV = 0;
                 for (unsigned i = 0; i < num_fs; i++) {
                     if (seqs[i] == 0)
                         continue; // sequence was discarded because it does not contain the root.
@@ -1113,7 +1113,7 @@ namespace algebraic_numbers {
 
                 unsigned num_rem  = 0; // number of remaining sequences
                 unsigned target_i = UINT_MAX; // index of sequence that is isolating
-                int target_lV, target_uV;
+                int target_lV = 0, target_uV = 0;
                 for (unsigned i = 0; i < num_fs; i++) {
                     if (seqs[i] == 0)
                         continue; // sequence was discarded because it does not contain the root.
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index cb86e2a85..762e8ceb2 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -540,7 +540,7 @@ namespace simplex {
         var_t max    = get_num_vars();
         var_t result = max;
         row r = row(m_vars[x_i].m_base2row);
-        int n;
+        int n = 0;
         unsigned best_col_sz = UINT_MAX;
         int best_so_far    = INT_MAX;
         
diff --git a/src/model/model_implicant.cpp b/src/model/model_implicant.cpp
index 44c70036c..0d37a04df 100644
--- a/src/model/model_implicant.cpp
+++ b/src/model/model_implicant.cpp
@@ -666,8 +666,8 @@ void model_implicant::eval_eq(app* e, expr* arg1, expr* arg2) {
 }
 
 void model_implicant::eval_basic(app* e) {
-    expr* arg1, *arg2;
-    expr *argCond, *argThen, *argElse, *arg;
+    expr* arg1 = 0, *arg2 = 0;
+    expr *argCond = 0, *argThen = 0, *argElse = 0, *arg = 0;
     bool has_x = false;
     unsigned arity = e->get_num_args();
     switch(e->get_decl_kind()) {
diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 5eb8e5f7e..e9b383b56 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -601,7 +601,7 @@ namespace datalog {
                 return;
             }
             while (!m_stack_P.empty()) {
-                unsigned on_stack_num;
+                unsigned on_stack_num = 0;
                 VERIFY( m_preorder_nums.find(m_stack_P.back(), on_stack_num) );
                 if (on_stack_num <= p_num) {
                     break;
@@ -710,7 +710,7 @@ namespace datalog {
                 item_set::iterator eend=deps.end();
                 for (; eit!=eend; ++eit) {
                     T * tgt = *eit;
-                    unsigned tgt_comp;
+                    unsigned tgt_comp = 0;
                     VERIFY( m_component_nums.find(tgt, tgt_comp) );
 
                     //m_components[tgt_comp]==0 means the edge is intra-component.
diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index e7babc719..6863a908f 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -836,7 +836,7 @@ namespace datalog {
         }
 
         void compile_eq(expr* e, expr_ref& result, var* v, unsigned hi, unsigned lo, expr* c) {
-            tbv* t;
+            tbv* t = 0;
             // TBD: hi, lo are ignored.
             VERIFY(m_expr2tbv.find(e, t));            
             var_ref w(m);
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 3a735165a..6dc93048a 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -274,7 +274,7 @@ namespace pdr {
 
         for (unsigned i = 0; i < src.size(); ) {
             expr * curr = src[i].get();
-            unsigned stored_lvl;
+            unsigned stored_lvl = 0;
             VERIFY(m_prop2level.find(curr, stored_lvl));
             SASSERT(stored_lvl >= src_level);
             bool assumes_level;
diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp
index 9af3ea8b4..934be5c63 100644
--- a/src/muz/pdr/pdr_util.cpp
+++ b/src/muz/pdr/pdr_util.cpp
@@ -247,7 +247,7 @@ namespace pdr {
         }
 
         bool test_eq(expr* e) const {
-            expr* lhs, *rhs;
+            expr* lhs = 0, *rhs = 0;
             VERIFY(m.is_eq(e, lhs, rhs));
             if (!a.is_int_real(lhs)) {
                 return true;
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 7fb2afd9e..0d4507971 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -466,7 +466,7 @@ namespace datalog {
 
         //used to save on filter_identical instructions where the check is already done 
         //by the join operation
-        unsigned second_tail_arg_ofs;
+        unsigned second_tail_arg_ofs = 0;
 
         // whether to dealloc the previous result
         bool dealloc = true;
diff --git a/src/muz/rel/dl_mk_partial_equiv.cpp b/src/muz/rel/dl_mk_partial_equiv.cpp
index d79a46720..94da7851f 100644
--- a/src/muz/rel/dl_mk_partial_equiv.cpp
+++ b/src/muz/rel/dl_mk_partial_equiv.cpp
@@ -109,7 +109,7 @@ namespace datalog {
             rule_vector const& rv = *(it->m_value);
             bool has_symmetry = false;
             bool has_transitivity = false;
-            unsigned i_symmetry, i_transitivity;
+            unsigned i_symmetry = 0, i_transitivity = 0;
             family_id kind = rm.get_requested_predicate_kind(p);
             for (unsigned i = 0; i < rv.size(); ++i) {
                 
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 0b0dae12c..7a73afd03 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -277,7 +277,7 @@ namespace datalog {
     relation_plugin & relation_manager::get_relation_plugin(family_id kind) {
         SASSERT(kind>=0);
         SASSERT(kind<m_next_relation_fid);
-        relation_plugin * res;
+        relation_plugin * res = 0;
         VERIFY(m_kind2plugin.find(kind, res));
         return *res;
     }
diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp
index 24fda3e96..f045bee4b 100644
--- a/src/muz/rel/dl_sparse_table.cpp
+++ b/src/muz/rel/dl_sparse_table.cpp
@@ -327,8 +327,7 @@ namespace datalog {
             key_value key;
             key.resize(key_len);
 
-            offset_vector * index_entry;
-            DEBUG_CODE( index_entry = 0; );
+            offset_vector * index_entry = 0;
             bool key_modified = true;
 
             for (; ofs!=after_last; ofs+=t.m_fact_size) {
diff --git a/src/muz/transforms/dl_mk_loop_counter.cpp b/src/muz/transforms/dl_mk_loop_counter.cpp
index 678bfc5a3..f97670ad0 100644
--- a/src/muz/transforms/dl_mk_loop_counter.cpp
+++ b/src/muz/transforms/dl_mk_loop_counter.cpp
@@ -56,7 +56,7 @@ namespace datalog {
 
     app_ref mk_loop_counter::del_arg(app* fn) {        
         expr_ref_vector args(m);
-        func_decl* old_fn, *new_fn = fn->get_decl();
+        func_decl* old_fn = 0, *new_fn = fn->get_decl();
         SASSERT(fn->get_num_args() > 0);
         args.append(fn->get_num_args()-1, fn->get_args());
         VERIFY (m_new2old.find(new_fn, old_fn));
diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp
index 48bd69255..048decaf9 100644
--- a/src/muz/transforms/dl_mk_magic_sets.cpp
+++ b/src/muz/transforms/dl_mk_magic_sets.cpp
@@ -264,7 +264,7 @@ namespace datalog {
         }
 
 
-        func_decl * new_head_pred;
+        func_decl * new_head_pred = 0;
         VERIFY( m_adorned_preds.find(adornment_desc(head->get_decl(), head_adornment), new_head_pred) );
         app * new_head = m.mk_app(new_head_pred, head->get_args());
 
diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp
index 48b41af56..7d103568a 100644
--- a/src/muz/transforms/dl_mk_unbound_compressor.cpp
+++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp
@@ -317,7 +317,6 @@ namespace datalog {
         unsigned tail_index = 0;
         while (tail_index < utail_len) {
             app * t = r->get_tail(tail_index);
-            func_decl * t_pred = t->get_decl();
 
             add_in_progress_indices(arg_indices, t);
 
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index 94c57e16d..a4d65d30b 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -140,7 +140,7 @@ class nlsat_tactic : public tactic {
             m_solver.set_display_var(m_display_var);
             
             lbool st = m_solver.check();
-            
+           
             if (st == l_undef) {
             }
             else if (st == l_true) {
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 3c2ac207c..7637da1e8 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -345,10 +345,9 @@ namespace opt {
     }
     
     expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) {
-		if (!val.is_finite())
-		{
-			return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m);
-		}
+        if (!val.is_finite()) {
+            return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m);
+        }
         smt::theory_opt& opt = get_optimizer();
         smt::theory_var v = m_objective_vars[var];
 
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 721e38942..4bf3c1580 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -362,7 +362,7 @@ namespace qe {
             }
             app* ite;
             if (find_ite(fml, ite)) {
-                expr* cond, *th, *el;
+                expr* cond = 0, *th = 0, *el = 0;
                 VERIFY(m.is_ite(ite, cond, th, el));
                 expr_ref tmp1(fml, m), tmp2(fml, m);
                 m_replace->apply_substitution(ite, th, tmp1);
diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index a4129d5cd..c2d0016c8 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -673,7 +673,7 @@ namespace qe {
         }
 
         unsigned find_max(model& mdl, bool do_pos) {
-            unsigned result;
+            unsigned result = 0;
             bool new_max = true;
             rational max_r, r;
             expr_ref val(m);
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 38861df65..3a909d6ba 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -2445,7 +2445,7 @@ public:
         }
                 
         virtual void assign(contains_app& x, expr* fml, rational const& vl) {
-            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/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp
index 088d2252d..78562cf00 100644
--- a/src/qe/qe_datatype_plugin.cpp
+++ b/src/qe/qe_datatype_plugin.cpp
@@ -792,9 +792,8 @@ namespace qe {
                 TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
             }
             else {
-                unsigned sz = m_datatype_util.get_datatype_num_constructors(s);
                 SASSERT(vl.is_unsigned());
-                SASSERT(vl.get_unsigned() < sz);
+                SASSERT(vl.get_unsigned() < m_datatype_util.get_datatype_num_constructors(s));
                 c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
             }
             subst_constructor(x, c, fml, def);                
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index f28a93753..2b73381a9 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -1667,7 +1667,7 @@ namespace fm {
             sbuffer<var>     xs;
             buffer<rational> as;
             rational         c;
-            bool             strict;
+            bool             strict = false;
             unsigned         num;
             expr * const *   args;
             if (m.is_or(f)) {
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index c60fb86cb..8db27c7ec 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -70,9 +70,9 @@ namespace sat {
                    tout << "watch_list:\n";
                    sat::display(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
                    tout << "\n";);
-            SASSERT(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
-            SASSERT(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
-            SASSERT(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
+            VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
+            VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
+            VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
         }
         else {
             if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 3a39af31b..8901c276f 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -42,7 +42,7 @@ namespace sat {
             // if it->get_kind() == BLOCK_LIT, then it might be the case that m[it->var()] != l_undef,
             // and the following procedure flips its value.
             bool sat = false;
-            bool var_sign;
+            bool var_sign = false;
             literal_vector::const_iterator it2  = it->m_clauses.begin();
             literal_vector::const_iterator end2 = it->m_clauses.end();
             for (; it2 != end2; ++it2) {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index fb1c98a74..65f62ec0e 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -381,7 +381,7 @@ private:
 
         m_core.reset();
         for (unsigned i = 0; i < core.size(); ++i) {
-            expr* e;
+            expr* e = 0;
             VERIFY(asm2dep.find(core[i].index(), e));
             m_core.push_back(e);
         }
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 0d7f6a3a6..ead1ea963 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2147,7 +2147,7 @@ namespace smt {
         enode_vector * best_v   = 0;
         for (unsigned i = 0; i < num_args; i++) {
             enode * bare          = c->m_joints[i];
-            enode_vector * curr_v;
+            enode_vector * curr_v = 0;
             switch (GET_TAG(bare)) {
             case NULL_TAG:
                 curr_v = 0;
diff --git a/src/smt/proto_model/value_factory.h b/src/smt/proto_model/value_factory.h
index 0bf0c7c98..f841e18ea 100644
--- a/src/smt/proto_model/value_factory.h
+++ b/src/smt/proto_model/value_factory.h
@@ -183,7 +183,7 @@ public:
         sort_info* s_info = s->get_info();
         sort_size const* sz = s_info?&s_info->get_num_elements():0;
         bool has_max = false;
-        Number max_size;
+        Number max_size(0);
         if (sz && sz->is_finite() && sz->size() < UINT_MAX) {
             unsigned usz = static_cast<unsigned>(sz->size());
             max_size = Number(usz);
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 711cdc336..530d0ec88 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -363,7 +363,7 @@ namespace smt {
               << ", scope_level: " << m_context.get_scope_level() << "\n";);
         if (m_params.m_qi_conservative_final_check) {
             bool  init = false;
-            float min_cost;
+            float min_cost = 0.0;
             unsigned sz = m_delayed_entries.size();
             for (unsigned i = 0; i < sz; i++) {
                 entry & e       = m_delayed_entries[i];
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 9c670e751..609181538 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2790,7 +2790,7 @@ void theory_seq::tightest_prefix(expr* s, expr* x) {
    (len(s) <= len(t) -> i <= len(t)-len(s))
 */
 void theory_seq::add_indexof_axiom(expr* i) {
-    expr* s, *t, *offset = 0;
+    expr* s = 0, *t = 0, *offset = 0;
     rational r;
     VERIFY(m_util.str.is_index(i, t, s) ||
            m_util.str.is_index(i, t, s, offset));
@@ -2891,7 +2891,7 @@ void theory_seq::add_elim_string_axiom(expr* n) {
  */
 void theory_seq::add_length_axiom(expr* n) {
     context& ctx = get_context();
-    expr* x;
+    expr* x = 0;
     VERIFY(m_util.str.is_length(n, x));
     if (m_util.str.is_concat(x) ||
         m_util.str.is_unit(x) ||
@@ -2914,7 +2914,7 @@ void theory_seq::add_length_axiom(expr* n) {
 }
 
 void theory_seq::add_itos_length_axiom(expr* len) {
-    expr* x, *n;
+    expr* x = 0, *n = 0;
     VERIFY(m_util.str.is_length(len, x));
     VERIFY(m_util.str.is_itos(x, n));
 
@@ -3295,7 +3295,7 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
 
 */
 void theory_seq::add_at_axiom(expr* e) {
-    expr* s, *i;
+    expr* s = 0, *i = 0;
     VERIFY(m_util.str.is_at(e, s, i));
     expr_ref len_e(m_util.str.mk_length(e), m);
     expr_ref len_s(m_util.str.mk_length(s), m);
@@ -4090,7 +4090,7 @@ void theory_seq::propagate_not_prefix2(expr* e) {
 
 void theory_seq::propagate_not_suffix(expr* e) {
     context& ctx = get_context();
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     VERIFY(m_util.str.is_suffix(e, e1, e2));
     literal lit = ctx.get_literal(e);
     SASSERT(ctx.get_assignment(lit) == l_false);
@@ -4119,7 +4119,7 @@ void theory_seq::propagate_not_suffix(expr* e) {
 */
 bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
     context& ctx = get_context();
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     VERIFY(m_util.str.is_prefix(e, e1, e2));
     SASSERT(ctx.get_assignment(e) == l_false);
     if (canonizes(false, e)) {
@@ -4191,7 +4191,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
  */
 bool theory_seq::add_suffix2suffix(expr* e, bool& change) {
     context& ctx = get_context();
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     VERIFY(m_util.str.is_suffix(e, e1, e2));
     SASSERT(ctx.get_assignment(e) == l_false);
     if (canonizes(false, e)) {
@@ -4276,7 +4276,7 @@ bool theory_seq::canonizes(bool sign, expr* e) {
 
 bool theory_seq::add_contains2contains(expr* e, bool& change) {
     context& ctx = get_context();
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     VERIFY(m_util.str.is_contains(e, e1, e2));
     SASSERT(ctx.get_assignment(e) == l_false);
     if (canonizes(false, e)) {
@@ -4346,7 +4346,7 @@ bool theory_seq::propagate_automata() {
 }
 
 void theory_seq::get_concat(expr* e, ptr_vector<expr>& concats) {
-    expr* e1, *e2;
+    expr* e1 = 0, *e2 = 0;
     while (true) {
         e = m_rep.find(e);
         if (m_util.str.is_concat(e, e1, e2)) {
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index eae3ab5e6..5c82bbbc3 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -993,7 +993,7 @@ class fm_tactic : public tactic {
             sbuffer<var>     xs;
             buffer<rational> as;
             rational         c;
-            bool             strict;
+            bool             strict = false;
             unsigned         num;
             expr * const *   args;
             if (m.is_or(f)) {
diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp
index 7a83ee403..7db3a15ca 100644
--- a/src/tactic/bv/elim_small_bv_tactic.cpp
+++ b/src/tactic/bv/elim_small_bv_tactic.cpp
@@ -147,11 +147,10 @@ class elim_small_bv_tactic : public tactic {
             expr_ref body(old_body, m);
             for (unsigned i = num_decls-1; i != ((unsigned)-1) && !max_steps_exceeded(num_steps); i--) {
                 sort * s = q->get_decl_sort(i);
-                symbol const & name = q->get_decl_name(i);
                 unsigned bv_sz = m_util.get_bv_size(s);
 
                 if (is_small_bv(s) && !max_steps_exceeded(num_steps)) {
-                    TRACE("elim_small_bv", tout << "eliminating " << name <<
+                    TRACE("elim_small_bv", tout << "eliminating " << q->get_decl_name(i) <<
                         "; sort = " << mk_ismt2_pp(s, m) <<
                         "; body = " << mk_ismt2_pp(body, m) << std::endl;);
 
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 0ee606da9..873dc55bc 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -176,7 +176,7 @@ private:
         app_map coloring;
         app_map depth;
         inv_app_map inv_color;
-        unsigned num_occs;
+        unsigned num_occs = 0;
         compute_sort_colors(fml, coloring);
         compute_max_depth(fml, depth);
         merge_colors(occs, coloring);        
@@ -233,7 +233,7 @@ private:
     typedef map<u_pair, unsigned, u_pair::hash, u_pair::eq> pair_map;
     bool merge_colors(app_map const& colors1, app_map& colors2) {
         pair_map recolor;
-        unsigned num_colors = 0, v1, v2, w, old_max = 0;
+        unsigned num_colors = 0, v1 = 0, v2 = 0, w = 0, old_max = 0;
         app_map::iterator it = colors2.begin(), end = colors2.end();
         for (; it != end; ++it) {
             app* a = it->m_key;
@@ -545,7 +545,7 @@ private:
         term_set& cts, term_set const& consts, app_map const& occs) {
         SASSERT(!T.empty());
         app* t = T[0];
-        unsigned weight, weight1;
+        unsigned weight = 0, weight1 = 0;
         VERIFY(occs.find(t, weight));
         unsigned cts_delta = compute_cts_delta(t, cts, consts);
         TRACE("symmetry_reduce", tout << mk_pp(t, m()) << " " << weight << " " << cts_delta << "\n";);
@@ -559,9 +559,9 @@ private:
             TRACE("symmetry_reduce", tout << mk_pp(t1, m()) << " " << weight1 << " " << cts_delta1 << "\n";);
             if ((t->get_num_args() == t1->get_num_args() && (weight1 > weight || cts_delta1 < cts_delta)) || 
                 t->get_num_args() > t1->get_num_args()) {
-                 cts_delta = cts_delta1;
-                 weight = weight1;
-                 t = t1;
+                cts_delta = cts_delta1;
+                weight = weight1;
+                t = t1;
             }
         }        
         return t;
diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
index 030d0bd8c..d8b016d7b 100644
--- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp
+++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
@@ -154,8 +154,7 @@ public:
 
         void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) {
             expr_ref old_pred(m.mk_app(f, num, args), m);
-            polarity_t pol;
-            VERIFY(m_polarities.find(old_pred, pol));
+            polarity_t pol = m_polarities.find(old_pred);
             result = m.mk_fresh_const(0, m.mk_bool_sort());
             m_polarities.insert(result, pol);
             m_new_preds.push_back(to_app(result));
diff --git a/src/tactic/tactical.h b/src/tactic/tactical.h
index 9aac3d42d..4b4274b0c 100644
--- a/src/tactic/tactical.h
+++ b/src/tactic/tactical.h
@@ -48,7 +48,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
 tactic * repeat(tactic * t, unsigned max = UINT_MAX); 
 /**
    \brief Fails if \c t produeces more than \c threshold subgoals.
-   Otherwise, it behabes like \c t.
+   Otherwise, it behaves like \c t.
 */
 tactic * fail_if_branching(tactic * t, unsigned threshold = 1);
 
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index d77b8c33f..03b720ae1 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1290,6 +1290,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
     m_mpz_manager.machine_div2k(Q_sig, sbits+3);
     renormalize(ebits, sbits, Q_exp, Q_sig);
 
+    (void)Q_sgn;
     TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl;
                          tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl;
                          tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;);
@@ -1310,6 +1311,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
     m_mpz_manager.mul(y.significand, Q_sig, YQ_sig);    
     renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits.
 
+    (void)YQ_sgn;
     TRACE("mpf_dbg_rem", tout << "YQ_sgn=" << YQ_sgn << std::endl;
                          tout << "YQ_exp=" << YQ_exp << std::endl;
                          tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl;