liquid-fixpoint-0.8.0.2: tests/horn/pos/icfp17-ex1.smt2

(fixpoint "--eliminate=horn")

(var $k ((Int)))

(constraint
  (forall ((x Int) (x >= 0))
    (and
      (forall ((v Int) (v = x - 1))
       (($k v)))
      (forall ((y Int) ($k y))
        (forall ((v Int) (v = y + 1))
          ((v >= 0)))))))