From our programs with arrays, we generate nonlinear Horn clauses over scalar variables only,in a common format with clear and unambiguous logical semantics, for which there exist several solvers. We thus avoid the use of solvers operating over arrays, which are still very immature.