@@ -248,20 +248,20 @@ bool code_contractst::apply_function_contract(
248
248
// TODO Generalize
249
249
if (ensures.id ()==ID_exists || ensures.id ()==ID_forall)
250
250
{
251
- exprt tup = ensures.operands ().front ();
252
- exprt q_var = tup .operands ().front ();
253
- symbol_exprt q_sym = to_symbol_expr (q_var );
254
-
255
- symbolt new_sym = get_fresh_aux_symbol (
256
- q_sym .type (),
257
- id2string (q_sym .get_identifier ()),
258
- " tmp" ,
259
- q_sym .source_location (),
260
- symbol_table.lookup_ref (function).mode ,
261
- symbol_table);
262
-
263
- symbol_exprt q (q_sym .get_identifier (), q_sym .type ());
264
- replace.insert (q, new_sym .symbol_expr ());
251
+ exprt tuple = ensures.operands ().front ();
252
+ exprt quantified_variable = tuple .operands ().front ();
253
+ symbol_exprt quantified_symbol = to_symbol_expr (quantified_variable );
254
+
255
+ symbolt new_symbol = get_fresh_aux_symbol (
256
+ quantified_symbol .type (),
257
+ id2string (quantified_symbol .get_identifier ()),
258
+ " tmp" ,
259
+ quantified_symbol .source_location (),
260
+ symbol_table.lookup_ref (function).mode ,
261
+ symbol_table);
262
+
263
+ symbol_exprt q (quantified_symbol .get_identifier (), quantified_symbol .type ());
264
+ replace.insert (q, new_symbol .symbol_expr ());
265
265
}
266
266
// Replace expressions in the contract components.
267
267
replace (assigns);
0 commit comments