fix #6600

ensure that semantics of last-indexof(t,"") = len(t)
Z3Prover · Feb 19, 2023 · 755b517 · 755b517
1 parent 0758c93
commit 755b517
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git 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
@@ -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;