diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c index fa2f19d9a10039567d3d3ff5bea533651dbd80c7..5f2a67576cc1348a143a6c2e67cc092e78fa397f 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c @@ -96,7 +96,7 @@ struct list *__e_acsl_f(struct list *l) if (! __e_acsl_at_3) __e_acsl_implies_2 = 1; else __e_acsl_implies_2 = __retres == __e_acsl_at_4; e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",(char *)"f", - (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==> \\result == \\old(l)", + (char *)"\\old(!\\valid{Here}(l) && !\\valid{Here}(l->next)) ==> \\result == \\old(l)", 20); __delete_block((void *)(& l)); __delete_block((void *)(& __retres));