Skip to content

Commit 7b3f0c1

Browse files
smowtonDaniel Kroening
authored and
Daniel Kroening
committed
is_not_zero: ensure equality test has exactly matching types
1 parent 512b6b7 commit 7b3f0c1

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)