No, it isn't. It's clearly undecidable. Herbrand equivalence is the best you can do (in general) if you are trying to say whether two variables have the same v

No, it isn't. It's clearly undecidable. Herbrand equivalence is the best you can do (in general) if you are trying to say whether two variables have the same values at the same program points. If you are willing to be probablistically correct you can do better, but you will get wrong answers (and not know they are wrong) That is likely okay for this application.