From 84da614de3cd2cb67118ebe7ab0764d74af4521c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Aug 2024 11:40:01 -0700 Subject: [PATCH] make gcc linting happy Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_legacy_frames.cpp | 4 ++-- src/muz/spacer/spacer_proof_utils.cpp | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp index a21df5038c4..15b37b1275a 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 9fbd4e01c2e..114dfc885d0 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 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);