mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-06 10:41:10 -07:00
parent 1935e86966
commit eed87807c5
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/arith_internalize.cpp
View file

@ -275,6 +275,9 @@ namespace arith {
else { else {
if (is_app(n)) { if (is_app(n)) {
internalize_args(to_app(n)); internalize_args(to_app(n));
for (expr* arg : *to_app(n))
if (a.is_arith_expr(arg))
internalize_term(arg);
} }
theory_var v = mk_evar(n); theory_var v = mk_evar(n);
coeffs[vars.size()] = coeffs[index]; coeffs[vars.size()] = coeffs[index];
@ -291,9 +294,8 @@ namespace arith {
st.to_ensure_enode().reset(); st.to_ensure_enode().reset();
for (unsigned i = st.to_ensure_var().size(); i-- > 0; ) { for (unsigned i = st.to_ensure_var().size(); i-- > 0; ) {
expr* n = st.to_ensure_var()[i]; expr* n = st.to_ensure_var()[i];
if (is_app(n)) { if (is_app(n))
internalize_term(to_app(n)); internalize_term(to_app(n));
}
} }
st.to_ensure_var().reset(); st.to_ensure_var().reset();
} }
@ -388,7 +390,6 @@ namespace arith {
return true; return true;
} }
bool solver::internalize_term(expr* term) { bool solver::internalize_term(expr* term) {
if (!has_var(term)) if (!has_var(term))
register_theory_var_in_lar_solver(internalize_def(term)); register_theory_var_in_lar_solver(internalize_def(term));
@ -424,7 +425,7 @@ namespace arith {
TRACE("arith", tout << mk_pp(t, m) << " " << force << " " << reflect(t) << "\n";); TRACE("arith", tout << mk_pp(t, m) << " " << force << " " << reflect(t) << "\n";);
if (!force && !reflect(t)) if (!force && !reflect(t))
return; return;
for (expr* arg : *t) for (expr* arg : *t)
e_internalize(arg); e_internalize(arg);
} }