@@ -146,17 +146,17 @@ mp_integer signedbv_typet::largest() const
146146
147147constant_exprt signedbv_typet::zero_expr () const
148148{
149- return to_constant_expr ( from_integer (0 , *this ) );
149+ return from_integer (0 , *this );
150150}
151151
152152constant_exprt signedbv_typet::smallest_expr () const
153153{
154- return to_constant_expr ( from_integer (smallest (), *this ) );
154+ return from_integer (smallest (), *this );
155155}
156156
157157constant_exprt signedbv_typet::largest_expr () const
158158{
159- return to_constant_expr ( from_integer (largest (), *this ) );
159+ return from_integer (largest (), *this );
160160}
161161
162162mp_integer unsignedbv_typet::smallest () const
@@ -171,15 +171,15 @@ mp_integer unsignedbv_typet::largest() const
171171
172172constant_exprt unsignedbv_typet::zero_expr () const
173173{
174- return to_constant_expr ( from_integer (0 , *this ) );
174+ return from_integer (0 , *this );
175175}
176176
177177constant_exprt unsignedbv_typet::smallest_expr () const
178178{
179- return to_constant_expr ( from_integer (smallest (), *this ) );
179+ return from_integer (smallest (), *this );
180180}
181181
182182constant_exprt unsignedbv_typet::largest_expr () const
183183{
184- return to_constant_expr ( from_integer (largest (), *this ) );
184+ return from_integer (largest (), *this );
185185}
0 commit comments