Parallel solving in SBV with Z3

Question

Referring to this answer, I'm trying the following to run Z3 in parallel from SBV:

runSMTWith z3{extraArgs = ["parallel.true"]} $ do ...

However, the above leads to the following exception:

*** Exception: 
*** Data.SBV: fd:21: hGetLine: end of file:
***
***    Sent      : (set-option :print-success true)
***
***    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.

If I remove extraArgs and simply go with the default thing (even using runSMT), the computation works perfectly well.

Answer 1

There was a typo in that answer. The correct invocation is:

runSMTWith z3{extraArgs = ["parallel.enabled=true"]} $ do ..

Try it like that and see if it works better.

Note that to debug these sorts of things, what SBV recommended is the right way to go. That is, run it with transcript=Just "bad.smt2" and feed bad.smt2 to z3 (or whichever solver you were using) with the same parameters outside of Haskell to see if there might be some other errors/warnings that are coming out of z3.