Variable names introduced in the frontend should be valid variables

[ehildenb]

Currently the K frontend introduces variables which are not valid for unmentioned portions of the configuration. For example, variable names like _1 and _2 are not valid.

This makes it hard to take the output of the prover and re-insert it into a later proof, or re-run it with a new execution, because the frontend parser does not handle it.

The frontend should only introduce valid variable names.

[radumereuta]

Find the step that introduces these names. Make sure we don't have collisions with the existing variables.