In this talk, I will present a machine for testing the convertibility of lambda-terms. This machine is based on implementations of strong call-by-need evaluation, and is able to exploit that convertibility is closed by context: to prove that f x is convertible with f y when f is a constant, it it enough to prove that x and y are convertible. However, it is sometimes more efficient to unfold f to prove convertibility, for instance if it does not use its argument. Our machine solves both convertibility problems in parallel while sharing computations, and stops as soon as it is able to conclude about the initial problem.