Craig Interpolation API

Question

There are versions of the Z3 SMT solver that support Craig interpolation. Methods of the API where, for example, Z3_interpolate, Z3_write_interpolation_problem, or Z3_mk_interpolation_context.

Microsoft Research provides a website with the description of the Z3 C API! The methods that are listed above cannot be found in this documentation. Have this methods been removed? Can they be found in a specific branch of Z3?

Answer 1

The documentation is for the master branch of Z3, newer features are available in the unstable branch, which will become the new master soon.

Answer 2

The code can be found (as of today; the code changes very frequently) in the branch "opt". The API functions were moved from z3_api.h to z3_interp.h. It is unclear whether the code will stay in this place or not.