Sort inference for variables

[ZachJHansen]

If we want to use Anthem to verify a program, that program's rules must contain variables that are variants of I,J,K etc if they are of an integer sort, and X,Y,Z, etc if they are of a program sort. A more user-friendly version would allow the input program to keep their expressive variable names and do the re-naming under the hood. I'm not sure how easy it would be to automatically infer sorts for program variables, or if the user would have to specify them explicitly. It may be something to discuss at the next Anthem meeting.