silicon icon indicating copy to clipboard operation
silicon copied to clipboard

Silicon cannot find z3 in PATH

Open JonasAlaif opened this issue 3 years ago • 0 comments

This change: https://github.com/viperproject/silicon/commit/d35ee70d5f64c021e5920f8544fef82768cf2462#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.

JonasAlaif avatar Jun 02 '22 08:06 JonasAlaif