fixed loop lower bound bug in loop info and default nullable value in…

… invalid_info
Z3Prover · Aug 21, 2020 · 7b478c8 · 7b478c8
1 parent 6b11af7
commit 7b478c8
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -429,7 +429,7 @@ class seq_util {
             /* 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. */