From 7b478c840650984af0870bbe96df9291b422af79 Mon Sep 17 00:00:00 2001
From: Margus Veanes <margus@microsoft.com>
Date: Fri, 21 Aug 2020 15:59:56 -0700
Subject: [PATCH] fixed loop lower bound bug in loop info and default nullable
value in invalid_info
---
src/ast/seq_decl_plugin.cpp | 2 +-
src/ast/seq_decl_plugin.h | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
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. */