janhaag/PSE2011 — Issue #106: Mangled variable names are somewhat cryptic
Author: janhaag
Created: 2012-03-07 03:57:53+00:00
State: open
Labels: Feature, Verifier/SMTLib

To resolve this, we might use a scheme based only on the position of variables in the sourcecode. I'd suggest something like
type@position
where type is one of "var", "qvar" and "array"; name is the actual variable name and position is LlCc where l and c are the line- and column number, respectively.

This scheme would not interfere with Z3 and it would still remove any ambiguity of the variable names, as the full position is unique by definition.