From efcad5ff358a9370e3ea5c57cb85bc59d21cc1af Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Tue, 26 Oct 2021 00:11:07 -0700 Subject: [PATCH] fixed nullability bug in the if-then-else info (#5620) --- src/ast/seq_decl_plugin.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 52edbdc80..ebae138e3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1703,7 +1703,13 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co // unsigned ite_min_length = std::min(min_length, i.min_length); // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef); // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted - return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, std::min(min_length, i.min_length), std::max(star_height, i.star_height)); + return info(false, false, false, false, + normalized && i.normalized, + monadic && i.monadic, + singleton && i.singleton, + ((nullable == l_true && i.nullable == l_true) ? l_true : ((nullable == l_false && i.nullable == l_false) ? l_false : l_undef)), + std::min(min_length, i.min_length), + std::max(star_height, i.star_height)); } else return i;