Revisiting Positive Equality

This paper provides a stronger result for exploiting positive equality in the logic of Equality with Uninterpreted Functions (EUF). Positive equality analysis is used to reduce the number of interpretations required to check the validity of a formula. We remove the primary restriction of the previous approach proposed by Bryant, German and Velev [5], where positive equality could be exploited only when all the function applications for a function symbol appear in positive context. We show that the set of interpretations considered by our analysis of positive equality is a subset of the set of interpretations considered by the previous approach. The paper investigates the obstacles in exploiting the stronger notion of positive equality (called robust positive equality) in a decision procedure and provides a solution for it. We present empirical results on some verification benchmarks.