mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix some build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-09-24 11:15:47 +01:00
parent afaa48d72a
commit a831fe9609
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz/spacer/spacer_global_generalizer.cpp
View file

@ -223,7 +223,7 @@ void lemma_global_generalizer::subsumer::setup_cvx_closure(
cc.reset(n_vars); cc.reset(n_vars);
unsigned bv_width; unsigned bv_width = 0;
if (contains_bv(m, lc.get_lemmas()[0].get_sub(), bv_width)) { if (contains_bv(m, lc.get_lemmas()[0].get_sub(), bv_width)) {
cc.set_bv(bv_width); cc.set_bv(bv_width);
} }
@ -232,7 +232,7 @@ void lemma_global_generalizer::subsumer::setup_cvx_closure(
cc.set_col_var(j, mk_rat_mul(m_col_lcm.get(j), m_col_names.get(j))); cc.set_col_var(j, mk_rat_mul(m_col_lcm.get(j), m_col_names.get(j)));
vector<rational> row; vector<rational> row;
unsigned i; unsigned i = 0;
for (const auto &lemma : lemmas) { for (const auto &lemma : lemmas) {
row.reset(); row.reset();
row.reserve(n_vars); row.reserve(n_vars);