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

fix heisenbug, unintialized variable, issue #720

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-09-10 11:04:29 -07:00
parent cb140011bc
commit 0b57829bdd
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1496,7 +1496,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
lchange = true; lchange = true;
} }
bool is_sat; bool is_sat = true;
unsigned szl = ls.size() - head1, szr = rs.size() - head2; unsigned szl = ls.size() - head1, szr = rs.size() - head2;
expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2; expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2;
@ -1693,11 +1693,11 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) { expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
expr* l, *r; expr* l, *r;
is_sat = true;
if (szl == 1 && m_util.str.is_itos(ls[0], l)) { if (szl == 1 && m_util.str.is_itos(ls[0], l)) {
if (szr == 1 && m_util.str.is_itos(rs[0], r)) { if (szr == 1 && m_util.str.is_itos(rs[0], r)) {
lhs.push_back(l); lhs.push_back(l);
rhs.push_back(r); rhs.push_back(r);
is_sat = true;
return true; return true;
} }
zstring s; zstring s;