viperproject/silicon

Silicon cannot find z3 in PATH

JonasAlaif opened this issue · 0 comments

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.