mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

fix #2764

Browse source 
fix #2764
This commit is contained in:
Nikolaj Bjorner 2019-12-01 12:05:58 -08:00
parent b371592c0d
commit 23fcc21543
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_diff_logic_def.h
View file

@ -389,21 +389,23 @@ template<typename Ext>
bool theory_diff_logic<Ext>::decompose_linear(app_ref_vector& terms, svector<bool>& signs) { bool theory_diff_logic<Ext>::decompose_linear(app_ref_vector& terms, svector<bool>& signs) {
for (unsigned i = 0; i < terms.size(); ++i) { for (unsigned i = 0; i < terms.size(); ++i) {
app* n = terms[i].get(); app* n = terms[i].get();
bool sign;
if (m_util.is_add(n)) { if (m_util.is_add(n)) {
expr* arg = n->get_arg(0); expr* arg = n->get_arg(0);
if (!is_app(arg)) return false; if (!is_app(arg)) return false;
expr_ref _n(n, get_manager());
terms[i] = to_app(arg); terms[i] = to_app(arg);
sign = signs[i];
for (unsigned j = 1; j < n->get_num_args(); ++j) { for (unsigned j = 1; j < n->get_num_args(); ++j) {
arg = n->get_arg(j); arg = n->get_arg(j);
if (!is_app(arg)) return false; if (!is_app(arg)) return false;
terms.push_back(to_app(arg)); terms.push_back(to_app(arg));
signs.push_back(signs[i]); signs.push_back(sign);
} }
--i; --i;
continue; continue;
} }
expr* x, *y; expr* x, *y;
bool sign;
if (m_util.is_mul(n, x, y)) { if (m_util.is_mul(n, x, y)) {
if (is_sign(x, sign) && is_app(y)) { if (is_sign(x, sign) && is_app(y)) {
terms[i] = to_app(y); terms[i] = to_app(y);