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

fixing issue #5140 (#5268)

Browse source
This commit is contained in:
Margus Veanes 2021-05-16 13:53:08 -07:00 • committed by GitHub
parent f942c3df91
commit 8ca6f567d3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/seq_decl_plugin.cpp
View file

@ -1480,7 +1480,7 @@ 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, 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, std::min(min_length, i.min_length), std::max(star_height, i.star_height));
}
else
return i;