Update our Yices2 bindings: Interpolation and Java bindings

[kfriedberger]

The newest (not yet released) version of Yices2 seems to support interpolation: Interpolation in the Yices2 API

Additionally, they seem to provide their own Java bindings, which might be worth a try.

We could update Yices2 when they release their next version.

[kfriedberger]

The interpolation is not yet sufficient for us, because it just provides some kind of unsat core. For our use case, we need a full interpolation between two arbitrary formulas.

[baierd]

Also, Yices2 supports arrays, while we do not. We should update Yices2 and incorporate arrays (and other new features).

[nianzelee]

Is there any update on this? According to their document, Section 1.4, Yices2 also supports arrays now.

The current Yices 2 release supports quantifier-free combinations of linear and non-linear integer and real arithmetic, uninterpreted function, arrays, and bitvectors