mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fix misc build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-11 17:41:24 -08:00
parent d97bd48669
commit 9a237d55ca
3 changed files with 2 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sls_arith_base.cpp
View file

@ -724,7 +724,6 @@ namespace sls {
for (auto idx : vi.m_adds) { for (auto idx : vi.m_adds) {
auto const& ad = m_adds[idx]; auto const& ad = m_adds[idx];
auto w = ad.m_var;
num_t sum(ad.m_coeff); num_t sum(ad.m_coeff);
for (auto const& [coeff, w] : ad.m_args) for (auto const& [coeff, w] : ad.m_args)
sum += coeff * value(w); sum += coeff * value(w);
@ -2265,7 +2264,7 @@ namespace sls {
return value(v) == (value(od.m_arg2) == 0 ? num_t(0) : mod(value(od.m_arg1), value(od.m_arg2))); return value(v) == (value(od.m_arg2) == 0 ? num_t(0) : mod(value(od.m_arg1), value(od.m_arg2)));
} }
case arith_op_kind::OP_POWER: { case arith_op_kind::OP_POWER: {
auto od = m_ops[vi.m_def_idx]; //auto od = m_ops[vi.m_def_idx];
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;
} }
@ -2333,7 +2332,6 @@ namespace sls {
display(out, ad) << "\n"; display(out, ad) << "\n";
} }
}; };
auto& out = verbose_stream();
for (var_t v = 0; v < m_vars.size(); ++v) { for (var_t v = 0; v < m_vars.size(); ++v) {
if (!eval_is_correct(v)) { if (!eval_is_correct(v)) {
report_error(verbose_stream(), v); report_error(verbose_stream(), v);

2
src/math/lp/lar_solver.cpp
View file

@ -699,7 +699,7 @@ namespace lp {
return; return;
lar_term t; lar_term t;
auto const& col = m_columns[j]; //auto const& col = m_columns[j];
auto const& r = basic2row(j); auto const& r = basic2row(j);
for (auto const& c : r) { for (auto const& c : r) {
if (c.var() != j) if (c.var() != j)

2
src/smt/smt_internalizer.cpp
View file

@ -1433,12 +1433,10 @@ namespace smt {
return nullptr; return nullptr;
case 1: { case 1: {
literal unit = lits[0]; literal unit = lits[0];
expr* atom = m_bool_var2expr[unit.var()];
if (j && !j->in_region()) if (j && !j->in_region())
m_justifications.push_back(j); m_justifications.push_back(j);
assign(unit, j); assign(unit, j);
inc_ref(unit); inc_ref(unit);
// m_units_to_reassert.push_back({ expr_ref(atom, m), unit.sign(), is_relevant(unit) });
return nullptr; return nullptr;
} }
case 2: case 2: