[Z3] Raise an error when Z3 cannot be executed
As discussed on #3385, the execution of Z3 has failed on MacOS because (the dependencies of) native libraries could not be resolved.
Since the problem can also occur on other platforms (e.g. because of an
erroneous update of Z3, problem introduced into OS specific RCP
application, change to OS such as introduction of System Integrity
Protection as discussed in #3385, an error dialog should be displayed
to the user in case Z3 cannot be executed. The current behavior is
“fail-silent”, apart from exceptions logged to the Eclipse
<workspace/.metadata/.log
file.
Testing
- Temporarily remove native libraries from developer installation
- First remove
libz3.{dll,so,dylib}
. It is required bylibz3java.{dll,so,dylib}
and should already raise an error - After reverting, remove
libz3java.{dll,so,dylib}
- On Windows, also test that the removal of the remaining DLLs (Visual Studio runtime etc.) is properly detected.
- First remove
- Testing in RCP product (e.g., from nightly build) is also recommended.
(from redmine: issue id 3387, created on 2018-04-18, closed on 2020-08-10)