@@ -95,8 +95,10 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
95
95
const function_application_exprt::argumentst &args=f.arguments ();
96
96
PRECONDITION (f.type ()==bool_typet () || f.type ().id ()==ID_c_bool);
97
97
PRECONDITION (args.size () == 2 || args.size () == 3 );
98
- const array_string_exprt &s0 = get_string_expr (args[swap_arguments ? 1 : 0 ]);
99
- const array_string_exprt &s1 = get_string_expr (args[swap_arguments ? 0 : 1 ]);
98
+ const array_string_exprt &s0 =
99
+ get_string_expr (args[swap_arguments ? 1u : 0u ]);
100
+ const array_string_exprt &s1 =
101
+ get_string_expr (args[swap_arguments ? 0u : 1u ]);
100
102
const exprt offset =
101
103
args.size () == 2 ? from_integer (0 , s0.length ().type ()) : args[2 ];
102
104
return typecast_exprt (add_axioms_for_is_prefix (s0, s1, offset), f.type ());
@@ -154,8 +156,10 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
154
156
155
157
symbol_exprt issuffix=fresh_boolean (" issuffix" );
156
158
typecast_exprt tc_issuffix (issuffix, f.type ());
157
- const array_string_exprt &s0 = get_string_expr (args[swap_arguments ? 1 : 0 ]);
158
- const array_string_exprt &s1 = get_string_expr (args[swap_arguments ? 0 : 1 ]);
159
+ const array_string_exprt &s0 =
160
+ get_string_expr (args[swap_arguments ? 1u : 0u ]);
161
+ const array_string_exprt &s1 =
162
+ get_string_expr (args[swap_arguments ? 0u : 1u ]);
159
163
const typet &index_type=s0.length ().type ();
160
164
161
165
implies_exprt a1 (issuffix, s1.axiom_for_length_ge (s0.length ()));
0 commit comments