Unexpected end-of-file error

[andrew-wja]

I'm using sbv 8.6, ghc 8.8.3 (the defaults from stack lts-15.12)

When I run the following simple program, I see:

*** Data.SBV: fd:73: hGetLine: end of file:
***
***    Sent      : (check-sat)
***
***    Executable: /usr/bin/z3
***    Options   : -nw -in -smt2

You can trigger this behaviour by uncommenting the commented lines from {- broken... and commenting the prior introduction of the as variable.

Am I trying to do something that I shouldn't here? The idea is to describe a model containing all lists of integers that could satisfy these constraints.

{-# LANGUAGE ScopedTypeVariables #-}
module Main where

import GHC.Exts (fromList)
import Data.SBV
import Data.SBV.Control
import Data.SBV.List ((.!!))
import Data.SBV.Tools.BoundedList
import qualified Data.SBV.List as L

example :: Symbolic [(Integer, Integer)]
example = do a :: SBV Integer <- exists "a"
             b :: SBV Integer <- exists "b"
             as <- return $ fromList [0,1,4,2,1,2,3,0]
             {- broken...
             as :: SBV [Integer] <- exists "as"
             constrain $ L.length as .== 8
             constrain $ ball 8 (.< 5) as
             constrain $ ball 8 (.>= 0) as
             -}
             constrain $ a `L.elem` as
             constrain $ (a `sMod` 2) .== 0
             constrain $ b `L.elem` as
             constrain $ b .>= a

             let run accum = do
                     cs <- checkSat
                     case cs of
                       Unk   -> error "Too bad, solver said unknown.." -- Won't happen
                       Unsat -> return accum
                       Sat   -> do av <- getValue a
                                   bv <- getValue b
                                   constrain $ (a ./= literal av) .|| (b ./= literal bv)
                                   run ((av, bv):accum)

             query $ do run []

main = do
  result <- runSMT example
  putStrLn $ show result

[andrew-wja]

Here is a simpler example that hilights exactly what triggers the error message:

example2 :: Symbolic [[Integer]]
example2 = do as :: SList Integer <- exists "as"
              constrain $ L.length as .== 4
              constrain $ ball 4 (.< 2) as
              constrain $ ball 4 (.>= 0) as

              let run accum = do
                      cs <- checkSat
                      case cs of
                        Unk   -> error "Too bad, solver said unknown.." -- Won't happen
                        Unsat -> return accum
                        Sat   -> do asv <- getValue as
                                    constrain $ as ./= fromList asv
                                    run (asv:accum)

              query $ do run []

I'm just describing a space of models including all binary strings of length exactly 4, modelled as lists of Integers (e.g. [0,1,1,0] and so on...)

I suspect I'm just trying to do something that I shouldn't here, but I can't imagine what that might be.

[LeventErkok]

Looks like you found a bug with z3 actually. I filed it here: https://github.com/Z3Prover/z3/issues/4324

Hopefully, the problem will just go away when they fix it in z3 and you update your version of z3. No change on the SBV side should be necessary.

As a side note, if you ever see this line:

*** Data.SBV: fd:73: hGetLine: end of file:

it almost always means the underlying SMT solver process died without responding. In such cases, you can use the transcript feature to get a set of commands, like this:

runSMTWith z3{transcript = Just "bug.smt2"} example2

The idea is that you can run it outside of SBV. And if you do, you'll see:

$ z3 bug.smt2
...bunch of lines...
[1]    11063 segmentation fault  z3 bug.smt2

This can help in identifying where the issue is. The generated transcript file is heavily commented as well, it contains time-stamps for debugging efficiency issues. Can be helpful in different scenarios.

I'll keep this ticket open till z3 folks fix the issue.

[andrew-wja]

Oh, that's really nice! I'll be using this feature a lot I suspect :D

[LeventErkok]

Just FYI. For this situation, we now generate the following message:

*** Exception:
*** Data.SBV: fd:15: hGetLine: end of file:
***
***    Sent      : (get-value (s0))
***
***    Executable: /usr/local/bin/z3
***    Options   : -nw -in -smt2
***
***    Hint      : Solver process prematurely ended communication.
***                It is likely it was terminated because of a seg-fault.
***                Run with 'transcript=Just "bad.smt2"' option, and feed
***                the generated "bad.smt2" file directly to the solver
***                outside of SBV for further information.

Hopefully this'll be less cryptic for users to deal with.

[LeventErkok]

@andrew-wja

Looks like z3-HEAD has fixed this issue. (You'll need to build from their github master).

I'm closing this ticket; please re-open if you find further issues.