Refinement Caml with Induction-based Horn Clause Solving

(The benchmark set used in our paper is available here)