File tree 1 file changed +10
-12
lines changed
1 file changed +10
-12
lines changed Original file line number Diff line number Diff line change @@ -864,20 +864,15 @@ bool simplify_exprt::simplify_extractbit(exprt &expr)
864
864
if (!is_bitvector_type (src_type))
865
865
return true ;
866
866
867
- std::size_t src_bit_width = to_bitvector_type (src_type).get_width ();
867
+ const std::size_t src_bit_width = to_bitvector_type (src_type).get_width ();
868
868
869
- if (extractbit_expr.index ().id () != ID_constant)
870
- {
871
- return true ;
872
- }
873
-
874
- auto index_converted_to_int =
869
+ const auto index_converted_to_int =
875
870
numeric_cast<mp_integer>(extractbit_expr.index ());
876
871
if (!index_converted_to_int.has_value ())
877
872
{
878
873
return true ;
879
874
}
880
- mp_integer index_as_int = index_converted_to_int.has_value ();
875
+ const mp_integer index_as_int = index_converted_to_int.value ();
881
876
if (!extractbit_expr.src ().is_constant ())
882
877
return true ;
883
878
@@ -887,12 +882,15 @@ bool simplify_exprt::simplify_extractbit(exprt &expr)
887
882
const irep_idt &src_value =
888
883
to_constant_expr (extractbit_expr.src ()).get_value ();
889
884
890
- if (src_value.size () != src_bit_width)
885
+
886
+ std::string src_value_as_string=id2string (src_value);
887
+
888
+ if (src_value_as_string.size () != src_bit_width)
891
889
return true ;
892
890
893
- bool bit =
894
- (id2string (src_value)
895
- [src_bit_width - numeric_cast_v<std::size_t >(index_as_int) - 1 ] == ' 1' );
891
+ const bool bit =
892
+ (src_value_as_string
893
+ [src_bit_width - numeric_cast_v<std::size_t >(index_as_int) - 1 ]== ' 1' );
896
894
897
895
expr.make_bool (bit);
898
896
You can’t perform that action at this time.
0 commit comments