"hGetLine: end of file" when using CVC4

[Altai-man]

My test file Test.lhs looks like this:

> module Test where

> {-@ hanoi :: Nat -> Nat @-}
> hanoi :: Int -> Int
> hanoi n | n == 1 = 1
>         | otherwise = 2 * (hanoi (n - 1)) + 1

ghc understands in perfectly, but liquid binary gives me:

➜  juice stack exec liquid src/Test.lhs 
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  Uniqify & Rename ***************************************************

Working  66% [============================================.....................]
liquid: fd:12: hGetLine: end of file

I built liquid executable from git yesterday using stack.

[ranjitjhala]

Hmm thanks for pointing this out! Did you build the develop branch?

[Altai-man]

Yes, I built develop branch. It was before your last merge. The exact commit I built from is 262631221de21671ee9b3aa8cf86cc9f07ed26a8. I can try latest version too if it is needed.

Also, this error prompts here and there when I try to use examples from the blog. For example, if I try code from this article - https://ucsd-progsys.github.io/liquidhaskell-blog/2013/12/14/gcd.lhs/, it will work perfectly for imports, gcd and mod functions. But if I add gcd' code, the error will appear.

[ranjitjhala]

hmm. can you try with the latest develop?

I just tried your code and it worked ok...

Also: what version of z3 do you have?

On Fri, Jan 27, 2017 at 9:14 AM, Altai-man notifications@github.com wrote:

Yes, I built develop branch. It was before your last merge. The exact commit I built from is 2626312 https://github.com/ucsd-progsys/liquidhaskell/commit/262631221de21671ee9b3aa8cf86cc9f07ed26a8. I can try latest version too if it is needed.

Also, this error prompts here and there when I try to use examples from the blog. For example, if I try code from this article - https://ucsd-progsys.github.io/liquidhaskell-blog/2013/12/14/gcd.lhs/, it will work perfectly for imports, gcd and mod functions. But if I add gcd' code, the error will appear.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/931#issuecomment-275719673, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOIDhY-PV2zqWh4lDhlbtawlEtZM3ks5rWiYLgaJpZM4Lv9Yt .

[Altai-man]

Okay, I've resolved it.

I used cvc4 as a prover. When you wrote about z3, I've emerged it, uninstalled cvc4 and now the error is gone! Hence closed.

Thanks to every liquidhaskell contributor for your awesome work on this project and quick response.

[gridaphobe]

@Altai-man we try to support cvc4 as well, would you mind telling us which version you had installed?

Thanks!

[Altai-man]

@gridaphobe, sure, sorry for early issue closing.

I'm on gentoo and my cvc4 version is 1.4-r1(the only one in the portage tree).

[gridaphobe]

@ranjitjhala here's the .smt2 file we pass to CVC4.

https://gist.github.com/anonymous/69d4cc5f59d83533b2c7e6bac47f1ed6

It produces

(error "Parse Error: .liquid/Foo.hs.smt2:165.3166: Symbol 'Z3_OP_MUL' not declared as a variable

  ...f$36$$35$$35$1677724517$35$$35$dL3 (Z3_OP_MUL lq_anf$36$$35$$35$167772...
                                         ^
")

Looks like our prelude for CVC4 (and probably MathSat) needs to be brought on par with Z3's.

[ranjitjhala]

Ah, thanks for keeping it open @gridaphobe -- I will fix this.

[ethanfrey]

By the way, I had similar problems with mathsat and cvc4 on osx. Details are in issue #990

There was also a syntax problem with my code, and when fixed, it worked with z3. Actually, everything works great with z3 and no pressure on my side to change the others. But I did test a few versions if you want to see the results.