Things to know when updating bindings

[meditans]

Hi,
as the bindings lack a number of features that are now in the Z3 C API, I'd like to try my hand at bringing it up to speed. Do you have any suggestion on gotchas, possible mistakes to be avoided, and suggested workflows, @IagoAbal? Is there there something in that API that shouldn't be bound, or can I just start from the beginning and work my way down?

[IagoAbal]

Hi @meditans, that would be very much appreciated. The main reason why we only cover a small subset of the C API is lack of time on my side, and I guess nobody has been interested enough in adding support for the uncovered parts.

I don't think there is any part of the API that cannot be covered.

As far as I can remember, there are two main things to be careful with. One is to check for errors after calling Z3 functions (see how it is done in other functions using withContextError, checkError, and toHsCheckError). The other one is to appropriately handle the refCount of the Z3 context when constructing/finalizing other Z3 objects, just look at the existing instances of the class Marshal.