elsoroka / Satisfiability.jl

Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.
https://elsoroka.github.io/Satisfiability.jl/
MIT License
28 stars 4 forks source link

An executable with the right name is not a sufficient condition for a working solver #40

Open elsoroka opened 6 months ago

elsoroka commented 6 months ago

Discovered while investigating issue #37 - If an executable (for example, cvc5) is present at the correct location but errors when run (perhaps because it's corrupt because the command for downloading it is outdated) this doesn't yield an error in Base.Process so the pipes open. But no solver is running so no responses are received & the process hangs.

There should be a simple way to fix this by sending a command to check the "liveness" of the solver when we open it and erroring if there's no response.