EqSat has been shown to be very successful for program optimizations and program equivalence checking, even when the given set of rewrite rules are not terminating or even when the theory is not decidable in general. However, despite its success in practice, there are no formal guarantees about EqSat: for example, when does EqSat terminate, and if it does not, how does one make it terminate. The first problem is known in the term rewriting literature as the termination problem, and the second is known as the completion problem. In this talk, we will focus on the termination problem of EqSat. In particular, we will show the following: (1) how the innocent-looking associativity rule can cause non-termination; (2) why a terminating, and even canonical, term rewriting system does not necessarily terminate in EqSat; (3) how to fix the above problem by “weakening” EqSat’s merge operation with its applications in rule synthesis; and (4) two potentially promising approaches to ensure the termination of EqSat.