From d861b912897b7ad25cc82844c7d997a0cc8feebd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jul 2019 11:13:05 +0100 Subject: [PATCH] augment axiomatization for substr to fix #2366 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 25e12b4eb..020ca748f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -724,7 +724,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)); } for (expr* rhs : other) { - t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs)); + t2 = m_autil.mk_add(t2, rhs); } result = m_util.str.mk_substr(t1, t2, c); return BR_REWRITE2;