From 1e839e5ac25e37b02e0ea9bebf67f2f6ac5474b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Nov 2024 19:42:13 -0800 Subject: [PATCH] add missing new_value_eh when repaired up Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_seq_plugin.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 3a85f3db77..ba52925d85 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -394,6 +394,7 @@ namespace sls { if (is_value(e)) return; strval0(e) = strval1(e); + ctx.new_value_eh(e); return; } @@ -1007,8 +1008,15 @@ namespace sls { auto& ev = get_eval(t); ev.max_length = 1; } - // extract with constant length. - + expr* x, * offset, * len; + rational len_r; + if (seq.str.is_extract(t, x, offset, len) && a.is_numeral(len, len_r)) { + auto& ev = get_eval(t); + if (len_r < 0) + ev.max_length = 0; + if (len_r.is_unsigned()) + ev.max_length = std::min(ev.max_length, len_r.get_unsigned()); + } } } @@ -1018,6 +1026,7 @@ namespace sls { if (!is_seq_predicate(e)) return; auto a = to_app(e); + // verbose_stream() << "repair " << lit << " " << mk_pp(e, m) << " " << bval1(e) << "\n"; if (bval1(e) == lit.sign()) ctx.flip(lit.var()); }