From 5c60c6662ca613c865e9b33d3d12186287dbe4b2 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Tue, 7 Jan 2025 18:26:00 +0100
Subject: [PATCH] Small seq-sls fixes (#7503)

* Calculation based on wrong update list

* Fixed regex problem
---
 src/ast/sls/sls_bv_lookahead.cpp |  1 -
 src/ast/sls/sls_seq_plugin.cpp   | 10 ++++++++--
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index dc67634a3..93cd6adf0 100644
--- 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
index 2ab01495a..9288b81c0 100644
--- 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;