Qualify Ghost Names

[rcosta358]

Summary

Added qualified names so ghosts/states with the same name from different classes don't conflict with each other.

Motivation

Different classes frequently reuse ghost/state names (e.g., open, close, size). Without qualification, simple name lookups collide, causing wrong substitutions and sort mismatches in the SMT solver.

Key Changes

• Qualified names: ghosts/states are stored and looked up with their declaring class prefix (e.g., java.util.ArrayList.size, com.example.SM1.initialized).
• Keep built-ins unqualified: old, length, addToIndex and getFromIndex.
• Safe resolution: VCChecker filters candidate ghosts/states to those whose prefix matches the types (and supertypes) of variables in the current VC, preventing unrelated classes with the same simple name from matching (removes ambiguity).
• Hierarchy-aware: added functionality in AuxStateHandler so subclasses can reference superclass states (Bus.close -> Car.close)
• Simple name fallback: added fallback in TranslatorToZ3to match by simple name and number of parameters, preferring exact qualified names.

[CatarinaGamboa]

This is a hugeee PR. I’m gonna stamp it for now since all tests are passing, it looks good overall and we discussed it offline, but we should try to split them into smaller pieces. For example, 1)add the new methods needed; 2) change call sites and add tests 3) remove unused code