From 6804c88b66fbdbdc8bba55487dbd6366352361fc Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 21 Mar 2017 12:54:06 -0400 Subject: [PATCH] make seq.extract rewrite type-generic --- 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 4f99c6ae6..526d715dc 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -517,13 +517,13 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu // case 1: pos<0 or len<0 // rewrite to "" if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) { - result = m_util.str.mk_string(symbol("")); + result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; } // case 1.1: pos >= length(base) // rewrite to "" if (constantBase && constantPos && pos.get_unsigned() >= s.length()) { - result = m_util.str.mk_string(symbol("")); + result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; }