Discuss loading of Z3 binary

[PhilippWendler]

The code that currently loads the Z3 binary in Z3SolverContext is

    if (NativeLibraries.OS.guessOperatingSystem() == NativeLibraries.OS.WINDOWS) {
      // Z3 itself
      System.loadLibrary("libz3");
      System.loadLibrary("libz3java");
    }

    System.loadLibrary("z3");
    System.loadLibrary("z3java");

This raises several questions:

• Why do we load z3 and z3java on Windows, too? Shouldn't this be an if-else construct?
• Do we want to explicitly load (lib)z3java? The Native class does it anyway (though it might be easier to understand if we do it, too?).
• Z3's Native class attempts to load z3java and on failure loads libz3java, we try to guess the OS instead of using a fallback. Both approaches have their advantages. Should we change to a fallback?

While we are at it, the code should get comments about why we load (lib)z3 explicitly, and why the name is different on Windows.

[cheshire]

Actually this never made sense to me, either, but I haven't tested it on Windows, so I don't know.
I think the whole if- block could (should?) be just removed.

@stahlbauer Any comments? I think you originally wrote this code, and you did have working Z3 under Windows at some stage.

[PhilippWendler]

We need some special handling for Windows, because on Linux when you load the library z3, actually a file named libz3.so is used (naming convention for libraries on Linux). On Windows when you load z3, it looks for a file named z3.dll. However, Z3 uses the Linux naming convention even for its Windows binaries, and thus the loadLibrary("z3") won't find anything on Windows. So we need either the if block, or a fall-back like the Native class does.

[cheshire]

@PhilippWendler If we ask user to move the .dll, I think we might as well ask them to rename it.
I think the problem is that now there are two shared objects, and maybe the way they serendipitously load under Linux (libz3j can't find libz3 but that's OK 'cause libz3 was already loaded) doesn't work.

[PhilippWendler]

I fear that renaming is error prone because it can be easily forgotten. E.g., when you want to update your existing Z3 version and just move the files without renaming, it will silently continue to use the old version.

[cheshire]

OK great thank you for fixing this! Does it mean we are fine under Windows now?

[PhilippWendler]

Yes, I just got final confirmation that it works, even with old Z3 release 4.4.1.