mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix crash caused by recycling variable names. Stackoverflow segfault-in-bv-rewritermk-mul-eq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-05 09:19:21 -08:00
parent 65de39f403
commit ee157e47e4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2064,12 +2064,12 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
} }
} }
if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) { if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) {
unsigned sz = to_app(rhs)->get_num_args(); unsigned num_args = to_app(rhs)->get_num_args();
unsigned i = 0; unsigned i = 0;
expr* c2, *x2; expr* c2, *x2;
numeral c2_val, c2_inv_val; numeral c2_val, c2_inv_val;
bool found = false; bool found = false;
for (; !found && i < sz; ++i) { for (; !found && i < num_args; ++i) {
expr* arg = to_app(rhs)->get_arg(i); expr* arg = to_app(rhs)->get_arg(i);
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) && if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
m_util.mult_inverse(c2_val, sz, c2_inv_val)) { m_util.mult_inverse(c2_val, sz, c2_inv_val)) {