mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-23 16:44:44 -07:00
parent 0b8177c7d6
commit b2bc51e9ac
1 changed files with 21 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/ast/rewriter/arith_rewriter.cpp
View file

@ -556,23 +556,29 @@ expr_ref arith_rewriter::remove_factor(expr* s, expr* t) {
return expr_ref(m_util.mk_mul(r.size(), r.data()), m);
}
}
expr_ref_vector sum(m);
sum.push_back(t);
for (unsigned i = 0; i < sum.size(); ++i) {
expr* arg = sum.get(i);
if (m_util.is_add(arg)) {
sum.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
sum[i] = sum.back();
sum.pop_back();
--i;
continue;
if (m_util.is_add(t)) {
expr_ref_vector sum(m);
sum.push_back(t);
for (unsigned i = 0; i < sum.size(); ++i) {
expr* arg = sum.get(i);
if (m_util.is_add(arg)) {
sum.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
sum[i] = sum.back();
sum.pop_back();
--i;
continue;
}
sum[i] = remove_factor(s, arg);
}
sum[i] = remove_factor(s, arg);
if (sum.size() == 1)
return expr_ref(sum.get(0), m);
else
return expr_ref(m_util.mk_add(sum.size(), sum.data()), m);
}
else {
SASSERT(s == t);
return expr_ref(m_util.mk_numeral(rational(1), m_util.is_int(t)), m);
}
if (sum.size() == 1)
return expr_ref(sum.get(0), m);
else
return expr_ref(m_util.mk_add(sum.size(), sum.data()), m);
}