mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

fix #3364

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-16 11:38:25 -07:00
parent a5c60ec517
commit 1bddfd40c3
2 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/poly_rewriter_def.h
View file

@ -766,7 +766,7 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
} }
if (move && num_coeffs == 0 && is_numeral(rhs)) { if (move && num_coeffs == 0 && is_numeral(rhs)) {
TRACE("mk_le_bug", tout << "no coeffs\n";); TRACE("mk_le_bug", tout << "no coeffs " << mk_pp(lhs, m()) << " = " << mk_pp(rhs, m()) << "\n";);
return BR_FAILED; return BR_FAILED;
} }
@ -788,8 +788,14 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
normalize(c); normalize(c);
if (!has_multiple && num_coeffs <= 1) { if (!has_multiple && num_coeffs <= 1) {
#if 0
if (num_coeffs == 0 || is_numeral(rhs)) {
return BR_FAILED;
}
#else
if (move) { if (move) {
if (is_numeral(rhs)) { if (is_numeral(rhs)) {
std::cout << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n";
return BR_FAILED; return BR_FAILED;
} }
} }
@ -798,7 +804,9 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
return BR_FAILED; return BR_FAILED;
} }
} }
#endif
} }
TRACE("le_bug", tout << num_coeffs << " " << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n";);
buffer<numeral> coeffs; buffer<numeral> coeffs;
m_expr2pos.reset(); m_expr2pos.reset();
@ -912,7 +920,7 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : nullptr; new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : nullptr;
lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset); lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset);
rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset); rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset);
TRACE("mk_le_bug", tout << lhs_result << " " << rhs_result << "\n";); TRACE("le_bug", tout << lhs_result << " " << rhs_result << "\n";);
return BR_DONE; return BR_DONE;
} }

2
src/smt/theory_arith_aux.h
View file

@ -1201,7 +1201,7 @@ namespace smt {
break; break;
} }
} }
if (idx == num_lits) { if (idx == num_lits || num_params == 0) {
return; return;
} }
for (unsigned i = 0; i < num_lits; ++i) { for (unsigned i = 0; i < num_lits; ++i) {