Re-enable Z3 4.5.0 for better interpolation (continuation of #536)

[baierd]

This PR continues the work from PR536 with support from our CI etc.

Original PR description from @leventeBajczi:
Old versions of z3 were really good at interpolation, and I want to add support for it in JavaSMT.

To this end, I've added the implementation of a Z3Legacy solver (to be renamed, as discussed with @baierd), which builds on the 4.5.0 release of z3, rebuilt to use com.microsoft.z3legacy as its package name to avoid name collisions with new z3.

Pre-built binaries with the modifications are available at https://github.com/leventeBajczi/z3/releases/tag/legacy-4.3.0-15644597379, which Theta already uses like this. This should be somehow integrated into the solver management of JavaSMT, which I have no experience with.

To demonstrate how good this version of Z3 is, I ran some preliminary tests in CPAchecker, and found that an NLA encoding of programs using Z3 as the interpolation solver in the predicate analysis configuration results in 510 successfully solved tasks, which are otherwise unsolved by the bitprecise encoding of the same tasks with mathsat5.

Also, I found that #381 (which I opened) is referenced in 3 of the tests, that now failed on this implementation. I removed the overly constraining line which expected the constraint IDs to be unique, which is not necessary IMO if the interpolation problem reported in that issue is otherwise handled - which it seems to be.

[leventeBajczi]

@kfriedberger: I see that in ac68cf8, you re-enabled the assertions I commented out. My understanding is that these tests are checking if my issue in #381 applies to the solver, but I don't think the equivalence of the handle for the formulas is necessarily a good way to test this. The issue was that a repeated addition of formulas made interpolation not work, and I think that tests should test exactly that -- and in this case, legacy Z3 fails the current tests, but otherwise pass the original issue's tests.
What do you think?

[kfriedberger]

@leventeBajczi points for noticing ✔️ The tests were just a smaller issue: Please do not disable tests that are intended for all solvers, when just adding one new solver, but rather use an assume-is-not-statement for LegacyZ3, if required. Additionally, there were several compiler warnings from around the disabled code that were not fixed properly. As soon as we get a properly compiled and released version of LegacyZ3 v4.5.0 included into JavaSMT (which we currently do not yet have managed), we will take another look at the tests.

[leventeBajczi]

Thanks, great!
(Just for the record -- I agree with not disabling tests in general, but in this case, I think that removing that assertion doesn't defeat the original purpose of the test IMO)

[kfriedberger]

@leventeBajczi and @baierd :
Is there any reason to use Z3 4.5.0 from 07-2016 instead of the latest version with interpolation support from around 05-2018? Was this just an example that provided interpolation support? The version from 2016 seems to suffer from parser issues (and some other issues 😄), maybe related to a bug with signed/unsigned-int. We might not fix such bugs within JavaSMT, as the used version of Z3 is quite outdated.