From 0fc9f1d46a4b35744e2c9061ff86e01b36b34657 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Oct 2021 16:20:32 -0700 Subject: [PATCH] fix max/min length to handle concatenation Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index cc78da8f6..8f3001055 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -932,7 +932,10 @@ unsigned seq_util::str::min_length(expr* s) const { return 0u; }; while (is_concat(s, s1, s2)) { - result += get_length(s1); + if (is_concat(s1)) + result += min_length(s1); + else + result += get_length(s1); s = s2; } result += get_length(s); @@ -960,7 +963,10 @@ unsigned seq_util::str::max_length(expr* s) const { return UINT_MAX; }; while (is_concat(s, s1, s2)) { - result = u.max_plus(get_length(s1), result); + if (is_concat(s1)) + result = u.max_plus(max_length(s1), result); + else + result = u.max_plus(get_length(s1), result); s = s2; } result = u.max_plus(get_length(s), result);