Towards Modularly Comparing Programs Using Automated Theorem Provers