return is a statement, and it's strange to have it as a variable to represent the return value.
Therefore, we could change it for result. But since result can be an actual variable that represents something other than the return value we, we can try using $result.
This would mean a small change in the grammar, probably, and a change in replacing the return value.
Ps: the _ should still work in any case
Example Before:
@Refinement("return > 0")
int test2 (){
return 10;
}
Example After:
@Refinement("$result > 0")
int test2 (){
return 10;
}