mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

make seq.extract rewrite type-generic

Browse source
This commit is contained in:
Murphy Berzish 2017-03-21 12:54:06 -04:00
parent 34717a7b6e
commit 6804c88b66
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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;
}