diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index 93192aefd..963da81cf 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -653,7 +653,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 ff951d4c1..9288b81c0 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -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;