A method which determines by an optimizing compiler whether any variable in the given program equals to the given acyclic mathematical function f(x,y, . . . ) applied to the given variables x, y, . . . in the program. In one embodiment, the method includes expressing the bits of the value of the function f(x,y, . . . ) as a Boolean function of the bits of the inputs x, y, . . . ; expressing, for every variable v and program statement s, the value taken by v when s is executed as a Boolean function V(s,v)(x, y, . . . ) of the bits of x, y, . . . ; and expressing, for every statement s, the condition under which the statement is executed as a Boolean function C(s)(x, y, . . . ) of the bits of the inputs x, y, . . . . Finally, a determination is made using a Boolean satisfiability oracle of whether, for the given variable v and program statement s, the following Boolean expression holds: C(s)(x,y, . . . )=>V(s,v)(x,y . . . )=f(x,y, . . . ). In a second embodiment, the method includes expressing the value of f(x,y, . . . ) as a plurality of functions fj(x,y, . . . ) having the corresponding predicate Pj(x,y, . . . ); expressing, for every variable v and program statement s, the value taken by v when s is executed as a plurality of functions Vj(s,v)(x,y, . . . ), one for each predicate Pj(x,y, . . . ); and expressing, for every statement s, the condition under which the statement is executed as a plurality of functions Cj(s)(x,y, . . . ), one for each predicate Pj(x,y, . . . ). Finally, a determination is of whether for the given variable v and program statement s, Vj(s,v)(x,y, . . . )=fj(x,y, . . . ) whenever the predicate Pj(x,y, . . . ) and the condition Cj(s)(x,y, . . . ) are true.