Skip to content

Commit 0225d20

Browse files
committed
is_not_zero: ensure equality test has exactly matching types
1 parent e3ff246 commit 0225d20

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/util/expr_util.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,8 @@ exprt is_not_zero(
115115
src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
116116

117117
exprt zero=from_integer(0, src_type);
118+
// Use tag type if applicable:
119+
zero.type() = src.type();
118120

119121
binary_relation_exprt comparison(src, id, std::move(zero));
120122
comparison.add_source_location()=src.source_location();

0 commit comments

Comments
 (0)