Constrained Horn Clause (CHC) is a universal format for formal verification problems. It is of great importance because it is expressive enough for any imperative programs written in different programming languages and any specifications to verify, …