diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5e6e03b7f..1d8f9f327 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1867,7 +1867,7 @@ seq_util::rex::info seq_util::rex::info::loop(unsigned lower) const { if (is_known()) { //r{l,m} is not normalized if r is nullable but l > 0 unsigned m = min_length * lower; - if (m < min_length || m < lower) + if (m > 0 && (m < min_length || m < lower)) m = UINT_MAX; bool loop_normalized = (nullable == l_false && lower > 0 ? false : normalized); lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index dd144530e..3298cd077 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -429,7 +429,7 @@ public: /* Positive Boolean combination of ranges or predicates or singleton sequences. */ bool singleton{ false }; /* If l_true then empty word is accepted, if l_false then empty word is not accepted. */ - lbool nullable{ l_false }; + lbool nullable{ l_undef }; /* Lower bound on the length of all accepted words. */ unsigned min_length{ 0 }; /* Maximum nesting depth of Kleene stars. */