diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp
index eea1938a6..f741d3fd4 100644
--- a/src/ast/substitution/substitution.cpp
+++ b/src/ast/substitution/substitution.cpp
@@ -85,7 +85,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
     m_state = APPLY;
 
     unsigned         j;
-    expr *           e;
+    expr *           e = 0;
     unsigned         off;
     expr_offset      n1;
     bool             visited;
@@ -214,7 +214,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
         }
     }
     SASSERT(m_apply_cache.contains(n));
-    m_apply_cache.find(n, e);
+    VERIFY(m_apply_cache.find(n, e));
     m_new_exprs.push_back(e);
     result = e;
     
diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp
index 1aef52d78..e00b1e9c0 100644
--- a/src/tactic/arith/elim01_tactic.cpp
+++ b/src/tactic/arith/elim01_tactic.cpp
@@ -169,7 +169,7 @@ public:
         for (; bit != bend; ++bit) {
             if (!is_app(*bit)) continue;
             app* x = to_app(*bit);
-            bool s1, s2;
+            bool s1 = false, s2 = false;
             rational lo, hi;
             if (a.is_int(x) && 
                 bounds.has_lower(x, lo, s1) && !s1 && zero <= lo &&
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 4c2e0dead..8f37a8d5e 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -176,7 +176,7 @@ public:
         bound_manager::iterator bit = bounds.begin(), bend = bounds.end();
         for (; bit != bend; ++bit) {
             expr* x = *bit;
-            bool s1, s2;
+            bool s1 = false, s2 = false;
             rational lo, hi;
             if (a.is_int(x) && 
                 bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() &&