Silicon cannot find z3 in PATH
JonasAlaif opened this issue · 0 comments
JonasAlaif commented
This change: d35ee70#diff-384bc38b113bf1202dd85dbd22ddee20345c21ef44a92fdde5fae2abd083ab7fR64-R70 added the .isFile
and .canExecute
checks for "z3", but in scala this only checks if ./z3
exists (it is not true that execute_command(z3Path) doesn't error ==> z3Path.isFile && z3Path.canExecute
since z3
can be found in the PATH). I'd suggest removing the checks here:
https://github.com/viperproject/silicon/blob/master/src/main/scala/decider/ProverStdIO.scala#L115-L119
And wrap this line:
https://github.com/viperproject/silicon/blob/master/src/main/scala/decider/ProverStdIO.scala#L136
in a try catch, if we really want to transform the IOException
into an ExternalToolError
.