liquid-fixpoint-8.10.7: tests/horn/pos/ple_sum.smt2

(fixpoint "--rewrite")
(fixpoint "--save")

(constant sum  (func(0, [int, int])))

(define sum(n : int) : int = { if (n <= 0) then (0) else (n + sum (n-1)) })

(constraint 
   (forall ((x int) (x == 5)) 
       (( (sum x) = 15 ))
   )
)