elsoroka/Satisfiability.jl

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

Opened this issue · 0 comments

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.