From 755b517001cf3f6926fd448a8e568e32efde0689 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Feb 2023 14:02:37 -0800 Subject: [PATCH] fix #6600 ensure that semantics of last-indexof(t,"") = len(t) --- src/ast/rewriter/seq_axioms.cpp | 4 ++-- src/util/zstring.cpp | 3 +-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 14f34f1f66a..e08ead08b71 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -513,8 +513,8 @@ namespace seq { !contains(t, s) => i = -1 |t| = 0 => |s| = 0 or i = -1 - |t| = 0 & |s| = 0 => i = 0 |t| != 0 & contains(t, s) => t = xsy & i = len(x) + |s| = 0 => i = len(t) |s| = 0 or s = s_head*s_tail |s| = 0 or !contains(s_tail*y, s) @@ -540,7 +540,7 @@ namespace seq { add_clause(cnt, i_eq_m1); add_clause(~t_eq_empty, s_eq_empty, i_eq_m1); - add_clause(~t_eq_empty, ~s_eq_empty, i_eq_0); + add_clause(~s_eq_empty, mk_eq(i, mk_len(t))); add_clause(t_eq_empty, ~cnt, mk_seq_eq(t, xsy)); add_clause(t_eq_empty, ~cnt, mk_eq(i, mk_len(x))); add_clause(s_eq_empty, mk_eq(s, mk_concat(s_head, s_tail))); diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp index 7d2b4296a54..570510458dd 100644 --- a/src/util/zstring.cpp +++ b/src/util/zstring.cpp @@ -214,8 +214,7 @@ int zstring::indexofu(zstring const& other, unsigned offset) const { } int zstring::last_indexof(zstring const& other) const { - if (length() == 0 && other.length() == 0) return 0; - if (other.length() == 0) return -1; + if (other.length() == 0) return length(); if (other.length() > length()) return -1; for (unsigned last = length() - other.length() + 1; last-- > 0; ) { bool suffix = true;