abstract_term_safely was called for each call data function argument. The same hash of _###SOLIDITY_ARG_VAR###_ was appended to each variable name as V{input.arg_name()}_hash. Input.arg_name is already sanitizing the name by prefixing it with V{index}_.
The internal representation looks like name => VV0_name_114b9705.
This PR is currently changing the internal representation to just KV0_name.
Functions like public getters have unnamed arguments, so we cannot drop the prefix.
Another requirement for symbolic vars in K is to start with an uppercase letter.
The prefix also helps with inputs that start with an _, because in K it is used to mark unused vars.
abstract_term_safely was called for each call data function argument. The same hash of
_###SOLIDITY_ARG_VAR###_was appended to each variable name asV{input.arg_name()}_hash.Input.arg_nameis already sanitizing the name by prefixing it withV{index}_.The internal representation looks like
name=>VV0_name_114b9705. This PR is currently changing the internal representation to justKV0_name.contracts.k has rules like these generated
Functions like public getters have unnamed arguments, so we cannot drop the prefix. Another requirement for symbolic vars in K is to start with an uppercase letter. The prefix also helps with inputs that start with an
_, because in K it is used to mark unused vars.