mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add code review comment

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-20 11:30:25 -07:00
parent b658934bd8
commit 8263d20e0d
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/seq_decl_plugin.cpp
View file

@ -1492,6 +1492,7 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) const {
if (is_known()) {
unsigned m = min_length * lower;
// Code review: this is not a complete overflow check.
if (m > 0 && (m < min_length || m < lower))
m = UINT_MAX;
lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable);