Improve error message when loading native solver fails

[PhilippWendler]

If a native solver cannot be loaded, JavaSMT throws an InvalidConfigurationException with the message

The SMT solver <name> is not available on this machine because of missing libraries (<reason>).
You may experiment with SMTInterpol by setting solver.solver=SMTInterpol.

This is nice for CPAchecker, but may be unfitting in other projects: maybe createSolverContext(Solvers) is used, such that the option solver.solver has no effect, and maybe SMTInterpol might not be available as well.

We have three possibilities:

1. Just change the exception message.
2. Introduce a new checked exception, e.g. SolverNotAvailableException.
3. Change to an unchecked exception, e.g. simply propagate the underlying UnsatisfiedLinkError.

Option 1 would have the disadvantage for CPAchecker that it would probably be difficult to still print this method (because we can't distinguish between this error and other problems). Option 2 would be backwards-incompatible if we do not make SolverNotAvailableException a subclass of InvalidConfigurationException. Option 3 would not be incompatible syntactically, but could still break existing applications that catch and handle the currently-thrown exception.

It's hard to decide what is the best option, because this depends on how JavaSMT is used. In some projects, solver instantiation may never be expected to fail, so an unchecked exception would be convenient. In other projects, the end user might be responsible for proper installation or choice of solvers, so in case of instantiation failure the application should not crash, so a checked exception would be good. In the end, we have to pick one and let applications that need the other way convert the exception as appropriately. Making it a checked exception would that this could not be forgotten. On the other hand, in the end this is something similar to a missing JAR file for a dependency, which is also typically an unchecked exception. We might even want to handle missing JARs for Java solvers and missing binaries for native solvers the same way in JavaSMT?

[cheshire]

and maybe SMTInterpol might not be available as well

Could it be? If JavaSMT is installed using Ivy or Maven, it is always available. If it's not, there would be a lot of missing dependencies. If the user is resolving dependencies manually, they probably would realize that they have to get SMTInterpol as well.

But you are indeed right that this is not a configuration issue, and that solver.solver option might not be a correct one.

[cheshire]

I personally prefer (3) for simplicity. Objections?