From 0b57829bddc59b147912c3cf1bcadc7a89e87a1a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Sep 2016 11:04:29 -0700 Subject: [PATCH] fix heisenbug, unintialized variable, issue #720 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0907ff4c7..4a82e5603 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1496,7 +1496,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ lchange = true; } - bool is_sat; + bool is_sat = true; unsigned szl = ls.size() - head1, szr = rs.size() - 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* l, *r; + is_sat = true; if (szl == 1 && m_util.str.is_itos(ls[0], l)) { if (szr == 1 && m_util.str.is_itos(rs[0], r)) { lhs.push_back(l); rhs.push_back(r); - is_sat = true; return true; } zstring s;