{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}

-- We locally define the operations null and length on integer lists
-- to avoid problems with polymorphism in Z3:
inull :: [Int] -> Bool
inull [] = True
inull (_:_) = False

-- last with recursive precondition:

minimum'pre :: [Int] -> Bool
minimum'pre xs = not (inull xs)

minimum :: [Int] -> Int
minimum [x] = x
minimum (x:xs@(_:_)) = min x (minimum xs)

--main1 = minimum [1..100000]