From 36e5d4dec9c01f87e6d6c5f2de3c202d84b2e92a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Nov 2017 11:01:44 -0800 Subject: [PATCH] fix #1377 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 13cb52df1..41b08a5d9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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;