From aff4b3022ad9a4c65364c82c2da3bcbd62052189 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jul 2019 10:57:52 -0700 Subject: [PATCH] fix #2417 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index eb6337e5a..63c881b93 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -731,6 +731,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs)); } result = m_util.str.mk_substr(t1, t2, c); + TRACE("seq", tout << result << "\n";); return BR_REWRITE2; } @@ -798,7 +799,7 @@ bool seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, rational& pos) { else { return false; } - return true; + return !pos.is_neg(); } bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {