mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix #1377

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-27 11:01:44 -08:00
parent 2b3ee995ff
commit 36e5d4dec9
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1572,6 +1572,8 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
bool lchange = false;
SASSERT(lhs.empty());
TRACE("seq", tout << ls << "\n"; tout << rs << "\n";);
//std::cout << ls << "\n";
//std::cout << rs << "\n";
// solve from back
while (true) {
while (!rs.empty() && m_util.str.is_empty(rs.back())) {
@ -1645,6 +1647,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
std::swap(l, r);
ls.swap(rs);
std::swap(head1, head2);
}
if (l == r) {
++head1;