diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp
index a21df5038..15b37b127 100644
--- a/src/muz/spacer/spacer_legacy_frames.cpp
+++ b/src/muz/spacer/spacer_legacy_frames.cpp
@@ -90,10 +90,10 @@ bool pred_transformer::legacy_frames::propagate_to_next_level(unsigned src_level
     for (unsigned i = 0; i < m_levels[src_level].size();) {
         expr_ref_vector &src = m_levels[src_level];
         expr * curr = src[i].get();
-        unsigned stored_lvl;
+        unsigned stored_lvl = 0;
         VERIFY(m_prop2level.find(curr, stored_lvl));
         SASSERT(stored_lvl >= src_level);
-        unsigned solver_level;
+        unsigned solver_level = 0;
         if (stored_lvl > src_level) {
             TRACE("spacer", tout << "at level: " << stored_lvl << " " << mk_pp(curr, m) << "\n";);
             src[i] = src.back();
diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp
index 9fbd4e01c..114dfc885 100644
--- a/src/muz/spacer/spacer_proof_utils.cpp
+++ b/src/muz/spacer/spacer_proof_utils.cpp
@@ -432,8 +432,8 @@ namespace spacer {
 
                 ptr_buffer<expr> args;
                 for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
-                    proof *pp, *tmp;
-                    pp = m.get_parent(p, i);
+                    proof *tmp = nullptr;
+                    proof* pp = m.get_parent(p, i);
                     VERIFY(m_cache.find(pp, tmp));
                     args.push_back(tmp);
                     dirty |= (pp != tmp);
@@ -455,8 +455,8 @@ namespace spacer {
             }
         }
 
-        proof* res;
-        VERIFY(m_cache.find(pr,res));
+        proof* res = nullptr;
+        VERIFY(m_cache.find(pr, res));
         DEBUG_CODE(
             proof_checker pc(m);
             expr_ref_vector side(m);