Skip to content

Commit b7caa0a

Browse files
author
Daniel Kroening
committed
cleanup mul_expr to use higher level functions
1 parent 4b5c41b commit b7caa0a

File tree

1 file changed

+9
-14
lines changed

1 file changed

+9
-14
lines changed

src/util/simplify_expr_int.cpp

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -119,12 +119,16 @@ static bool mul_expr(
119119

120120
const irep_idt &type_id=dest.type().id();
121121

122-
if(type_id==ID_integer || type_id==ID_natural)
122+
if(
123+
type_id == ID_integer || type_id == ID_natural ||
124+
type_id == ID_unsignedbv || type_id == ID_signedbv)
123125
{
124-
dest.set_value(integer2string(
125-
string2integer(id2string(dest.get_value()))*
126-
string2integer(id2string(expr.get_value()))));
127-
return false;
126+
mp_integer a, b;
127+
if(!to_integer(dest, a) && !to_integer(expr, b))
128+
{
129+
dest = from_integer(a * b, dest.type());
130+
return false;
131+
}
128132
}
129133
else if(type_id==ID_rational)
130134
{
@@ -135,15 +139,6 @@ static bool mul_expr(
135139
return false;
136140
}
137141
}
138-
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
139-
{
140-
// the following works for signed and unsigned integers
141-
dest.set_value(integer2binary(
142-
binary2integer(id2string(dest.get_value()), false)*
143-
binary2integer(id2string(expr.get_value()), false),
144-
to_bitvector_type(dest.type()).get_width()));
145-
return false;
146-
}
147142
else if(type_id==ID_fixedbv)
148143
{
149144
fixedbvt f(to_constant_expr(dest));

0 commit comments

Comments
 (0)