From 2d10779f4abe6a9873c0207e29b1bf53305fa5a2 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 7 Jan 2025 11:01:07 +0100 Subject: [PATCH] Fixed regex problem --- src/ast/sls/sls_bv_lookahead.cpp | 1 - src/ast/sls/sls_seq_plugin.cpp | 8 +++++++- 2 files changed, 7 insertions(+), 2 deletions(-) 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;