Small seq-sls fixes (#7503)

* Calculation based on wrong update list * Fixed regex problem
Z3Prover · Jan 7, 2025 · 5c60c66 · 5c60c66
1 parent e133a29
commit 5c60c66
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
@@ -658,7 +658,6 @@ namespace sls {
             return false;
 
         SASSERT(is_uninterp(t));
-        SASSERT(m_restore.empty());
 
         if (bv.is_bv(t)) {
             wval(t).eval = new_value;

diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
@@ -1676,7 +1676,7 @@ namespace sls {
             if (!is_str_update) {
                 i = m_int_updates.size();
                 do {
-                    lim -= m_str_updates[--i].m_score;
+                    lim -= m_int_updates[--i].m_score;
                 } while (lim >= 0 && i > 0);
             }
 
@@ -2066,7 +2066,13 @@ namespace sls {
                     return append_char(r0, r, s);
                 }
             }
-            NOT_IMPLEMENTED_YET();
+            expr* r2;
+            do {
+                r2 = to_app(r)->get_arg(ctx.rand(to_app(r)->get_num_args()));
+            } while (r2 == r0);
+            r = r2;
+            // Just take one that is not a self loop (there is always such one element)
+            return append_char(r0, r, s);
         }
         if (m.is_ite(r, c, th, el)) {
             unsigned low = 0, high = UINT_MAX;