Proving correctness of imperative programs by linearizing constrained horn clauses