@@ -210,8 +210,8 @@ __CPROVER_HIDE:;
210210CAR_SET_CONTAINS_LOOP :
211211 while (idx != 0 )
212212 {
213- incl |= candidate .is_writable & elem -> is_writable &
214- __CPROVER_same_object (elem -> lb , candidate .lb ) &
213+ incl |= ( int ) candidate .is_writable & ( int ) elem -> is_writable &
214+ ( int ) __CPROVER_same_object (elem -> lb , candidate .lb ) &
215215 (__CPROVER_POINTER_OFFSET (elem -> lb ) <=
216216 __CPROVER_POINTER_OFFSET (candidate .lb )) &
217217 (__CPROVER_POINTER_OFFSET (candidate .ub ) <=
@@ -798,7 +798,7 @@ __CPROVER_HIDE:;
798798 while (idx != 0 )
799799 {
800800 incl |=
801- elem -> is_writable & __CPROVER_same_object (elem -> lb , ptr ) &
801+ ( int ) elem -> is_writable & ( int ) __CPROVER_same_object (elem -> lb , ptr ) &
802802 (__CPROVER_POINTER_OFFSET (elem -> lb ) <= offset ) &
803803 (__CPROVER_POINTER_OFFSET (ub ) <= __CPROVER_POINTER_OFFSET (elem -> ub ));
804804 ++ elem ;
@@ -1045,8 +1045,9 @@ __CPROVER_HIDE:;
10451045 // call free only iff the pointer is valid preconditions are met
10461046 // skip checks on r_ok, dynamic_object and pointer_offset
10471047 __CPROVER_bool preconditions =
1048- (ptr == 0 ) | (__CPROVER_r_ok (ptr , 0 ) & __CPROVER_DYNAMIC_OBJECT (ptr ) &
1049- (__CPROVER_POINTER_OFFSET (ptr ) == 0 ));
1048+ (ptr == 0 ) |
1049+ ((int )__CPROVER_r_ok (ptr , 0 ) & (int )__CPROVER_DYNAMIC_OBJECT (ptr ) &
1050+ (__CPROVER_POINTER_OFFSET (ptr ) == 0 ));
10501051 // If there is aliasing between the pointers in the freeable set,
10511052 // and we attempt to free again one of the already freed pointers,
10521053 // the r_ok condition above will fail, preventing us to deallocate
0 commit comments