liquid-fixpoint-8.10.7: tests/horn/pos/ple0.smt2
(fixpoint "--rewrite")
(constant adder (func(0, [int, int, int])))
(define adder(x : int, y : int) : int = { x + y })
(constraint
(forall ((x int) (x == 5))
(forall ((y int) (y == 6))
(( (adder x y) = 11 ))
)
)
)