Avoid generating ghost state declarations for quantifiers unless quantifiers are used

[wuestholz]

Currently, ghost state declarations (e.g., for tracking map keys) are generated regardless of whether there is a quantifier that quantifies over the corresponding map. It would be great to only generate the declarations on demand.

[cd1m0]

Is this in the case where there is a sum operator over the map, but no forall?

[wuestholz]

Yeah, I think that was the case.