@@ -146,17 +146,17 @@ mp_integer signedbv_typet::largest() const
146
146
147
147
constant_exprt signedbv_typet::zero_expr () const
148
148
{
149
- return to_constant_expr ( from_integer (0 , *this ) );
149
+ return from_integer (0 , *this );
150
150
}
151
151
152
152
constant_exprt signedbv_typet::smallest_expr () const
153
153
{
154
- return to_constant_expr ( from_integer (smallest (), *this ) );
154
+ return from_integer (smallest (), *this );
155
155
}
156
156
157
157
constant_exprt signedbv_typet::largest_expr () const
158
158
{
159
- return to_constant_expr ( from_integer (largest (), *this ) );
159
+ return from_integer (largest (), *this );
160
160
}
161
161
162
162
mp_integer unsignedbv_typet::smallest () const
@@ -171,15 +171,15 @@ mp_integer unsignedbv_typet::largest() const
171
171
172
172
constant_exprt unsignedbv_typet::zero_expr () const
173
173
{
174
- return to_constant_expr ( from_integer (0 , *this ) );
174
+ return from_integer (0 , *this );
175
175
}
176
176
177
177
constant_exprt unsignedbv_typet::smallest_expr () const
178
178
{
179
- return to_constant_expr ( from_integer (smallest (), *this ) );
179
+ return from_integer (smallest (), *this );
180
180
}
181
181
182
182
constant_exprt unsignedbv_typet::largest_expr () const
183
183
{
184
- return to_constant_expr ( from_integer (largest (), *this ) );
184
+ return from_integer (largest (), *this );
185
185
}
0 commit comments