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 initialization of mod terms

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 15:01:50 -08:00
parent fd5f5feb40
commit 632e2b56e4
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -504,8 +504,8 @@ namespace sls {
add_update(mk_term(e), delta_out); add_update(mk_term(e), delta_out);
} }
else { else {
if (!is_uninterp(vi.m_expr) && m_allow_recursive_delta) IF_VERBOSE(3, if (!is_uninterp(vi.m_expr) && m_allow_recursive_delta)
verbose_stream() << mk_bounded_pp(vi.m_expr, m) << " += " << delta_out << "\n"; verbose_stream() << mk_bounded_pp(vi.m_expr, m) << " += " << delta_out << "\n");
m_updates.push_back({ v, delta_out, 0 }); m_updates.push_back({ v, delta_out, 0 });
} }
} }
@ -1027,7 +1027,7 @@ namespace sls {
num_t val; num_t val;
switch (k) { switch (k) {
case arith_op_kind::OP_MOD: case arith_op_kind::OP_MOD:
val = value(vy) == 0 ? num_t(0) : mod(value(v), value(vy)); val = value(vy) == 0 ? num_t(0) : mod(value(vx), value(vy));
break; break;
case arith_op_kind::OP_REM: case arith_op_kind::OP_REM:
if (value(vy) == 0) if (value(vy) == 0)
@ -1063,7 +1063,7 @@ namespace sls {
m_vars[v].m_op = k; m_vars[v].m_op = k;
m_vars[v].set_value(val); m_vars[v].set_value(val);
m_vars[vx].m_ops.push_back(v); m_vars[vx].m_ops.push_back(v);
TRACE("arith", display(tout << "initialize op ", v) << " " << value(vx) << " " << value(vy) << "\n"); TRACE("arith", display(tout << "initialize op ", v) << " " << value(vx) << " op " << value(vy) << "\n");
if (vy != vx) if (vy != vx)
m_vars[vy].m_ops.push_back(v); m_vars[vy].m_ops.push_back(v);
return v; return v;
@ -1374,7 +1374,7 @@ namespace sls {
if (!vi.is_arith_op()) if (!vi.is_arith_op())
return false; return false;
flet<bool> _tabu(m_use_tabu, false); flet<bool> _tabu(m_use_tabu, false);
TRACE("sls", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"); TRACE("sls_verbose", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
switch (vi.m_op) { switch (vi.m_op) {
case arith_op_kind::LAST_ARITH_OP: case arith_op_kind::LAST_ARITH_OP:
break; break;
@ -2524,7 +2524,7 @@ namespace sls {
if (!vi.is_arith_op()) if (!vi.is_arith_op())
return true; return true;
IF_VERBOSE(10, verbose_stream() << vi.m_op << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"); IF_VERBOSE(10, verbose_stream() << vi.m_op << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
TRACE("sls", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"); TRACE("sls_verbose", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n");
switch (vi.m_op) { switch (vi.m_op) {
case arith_op_kind::LAST_ARITH_OP: case arith_op_kind::LAST_ARITH_OP:
break; break;