based on http://web.cs.iastate.edu/~weile/docs/xie_fse16.pdf fig1a (originially from [28])

xie16_1a.hs

{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--noterm" @-}

module Test (indirect, snd3, fst3, thd3) where

{-@ reflect snd3 @-}
snd3 (x,y,z) = y

{-@ reflect fst3 @-}
fst3 (x,y,z) = x

{-@ reflect thd3 @-}
thd3 (x,y,z) = z

-- I worked out the CNF of this on paper, and it is a 3CNF over our predicates,
-- but no way in hell I'm typing it out
{-@ indirect :: x:Int -> z:Int -> n:Int -> {v:_ | (x == fst3 v && z == thd3 v) || (x == fst3 v && z == snd3 v) || (x == thd3 v && z == snd3 v)} @-}
indirect :: Int -> Int -> Int -> (Int,Int,Int)
indirect x z n = count x z n

count :: Int -> Int -> Int -> (Int,Int,Int)
count x z n =
    if   x < n
    then if z < x
         then count (x+1) z n
         else count x (z+1) n
    else (x,z,n)

-- int n:= ∗ ;
-- int x:= ∗ ;
-- int z:= ∗ ;
-- while (x<n)
-- -- if (z>x)  x++;
-- -- else z++;
-- assert (x==z)