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

fix build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-10 11:51:21 -08:00
parent af270da785
commit 62126fd6e2
4 changed files with 13 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -497,7 +497,7 @@ namespace sls {
else if (is_op(v) && m_allow_recursive_delta)
add_update(get_op(v), delta_out);
else if (vi.is_if_op() && m_allow_recursive_delta) {
expr* c, * t, * e;
expr* c = nullptr, * t = nullptr, * e = nullptr;
VERIFY(m.is_ite(vi.m_expr, c, t, e));
bool cond = ctx.is_true(c);
if (cond)
@ -540,7 +540,6 @@ namespace sls {
num_t arg2 = value(od.m_arg2);
if (arg2 != 0) {
num_t val = div(arg1, arg2);
if (arg2 > 0)
add_update(od.m_arg1, delta * arg2);
else if (arg2 < 0)
@ -550,7 +549,6 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::add_update_mod(op_def const& od, num_t const& delta) {
num_t val = value(od.m_var);
num_t arg1 = value(od.m_arg1);
num_t arg2 = value(od.m_arg2);
if (arg1 + delta >= 0 && arg1 + delta < arg2)

5
src/ast/sls/sls_arith_clausal.cpp
View file

@ -60,7 +60,8 @@ namespace sls {
else if ((!m_bool_mode && bool_in_unsat > 0 && time_up_arith) || vars_in_unsat == bool_in_unsat)
enter_bool_mode();
if (m_bool_mode) {
bv = ctx.bool_flip();
bv = ctx.bool_flip();
m_no_improve_bool = update_outer_best_solution() ? 0 : m_no_improve_bool + 1;
}
else {
@ -69,6 +70,8 @@ namespace sls {
}
m_no_improve = update_best_solution() ? 0 : m_no_improve + 1;
(void)bv;
(void)v;
TRACE("arith",
if (bv != sat::null_bool_var) tout << "bool flip " << bv << "\n";
else if (v != null_arith_var) tout << "arith flip v" << v << "\n";

3
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -310,6 +310,7 @@ namespace sls {
out << g->bpp(sib) << " ";
out << " <- " << mk_bounded_pp(m_values.get(n->get_id()), m) << "\n";
};
(void)trace_assignment;
deps.topological_sort();
expr_ref_vector args(m);
euf::enode_vector leaves, worklist;
@ -943,7 +944,7 @@ namespace sls {
for (expr* b : m_occurs[f]) {
if (b == e)
continue;
expr* a;
expr* a = nullptr;
VERIFY(dt.is_accessor(b, a));
auto v_a = eval0(a);
if (v_a.get() == t) {

12
src/ast/sls/sls_seq_plugin.cpp
View file

@ -575,7 +575,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_length(app* e) {
expr* x;
expr* x = nullptr;
VERIFY(seq.str.is_length(e, x));
expr_ref len = ctx.get_value(e);
rational r;
@ -603,7 +603,7 @@ namespace sls {
}
void seq_plugin::repair_up_str_stoi(app* e) {
expr* x;
expr* x = nullptr;
VERIFY(seq.str.is_stoi(e, x));
rational val_e;
@ -622,7 +622,7 @@ namespace sls {
}
void seq_plugin::repair_up_str_itos(app* e) {
expr* x;
expr* x = nullptr;
VERIFY(seq.str.is_itos(e, x));
rational val_x;
VERIFY(a.is_numeral(ctx.get_value(x), val_x));
@ -670,7 +670,7 @@ namespace sls {
bool seq_plugin::repair_down_str_eq(app* e) {
bool is_true = ctx.is_true(e);
expr* x, * y;
expr* x = nullptr, * y = nullptr;
VERIFY(m.is_eq(e, x, y));
IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n");
if (ctx.is_true(e)) {
@ -1830,7 +1830,7 @@ namespace sls {
expr_ref val(m);
for (auto lit : ctx.unit_literals()) {
auto e = ctx.atom(lit.var());
expr* x, * y, * z;
expr* x = nullptr, * y = nullptr, * z = nullptr;
rational r;
if (!lit.sign() && (a.is_le(e, x, y) || a.is_ge(e, y, x))) {
if (a.is_numeral(x, r) && r.is_unsigned() && seq.str.is_length(y, z)) {
@ -2029,7 +2029,7 @@ namespace sls {
if (m.is_eq(x, ))
}
#endif
expr* x, * y;
expr* x = nullptr, * y = nullptr;
zstring s;
if (seq.re.is_concat(r, x, y)) {
auto info = seq.re.get_info(x);