The function that tests for register equality explicitly ignores the instruction pointer (as we usually don't want to assume or prove anything about it). This is somewhat a conflation of concerns, as this should instead be handled by the equivalence domain.
The function that tests for register equality explicitly ignores the instruction pointer (as we usually don't want to assume or prove anything about it). This is somewhat a conflation of concerns, as this should instead be handled by the equivalence domain.