attempted `reflect` with "builtin symbol" causes crash

[awstlaur]

I have the following code in foo.hs:

import Prelude hiding (rem)

{-@ rem :: Nat -> {v:Nat | v /= 0} -> Nat @-}
rem :: Int -> Int -> Int
rem x n --- | n == 0    = error "divide by zero"
        | x == 0    = 0
        | x > n     = rem (x - n) n
        | otherwise = x

{-@ reflect rem @-}

and, when I run liquid foo.hs, I get:

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 154 column 30: invalid declaration, builtin symbol rem"

If I remove the reflect attempt, it's fine. If I rename rem to foo then it's able to carry out the reflect.

[nikivazou]

Seems that rem is a symbol defined in the SMT logic and cannot be redifined as an uninterpreted function. Change the name of your function to something like haskellRem or myRem

[awstlaur]

Yeah, I ended up going with remainder which worked fine. If it's feasible to improve the error reporting in such cases then I'd vote for keeping this issue open.

[nikivazou]

Sure, thanks!