Proving correctness of imperative programs by linearizing constrained Horn clauses