The .NET binding of Z3 seems to miss an implementation for assert_and_track in the Optimize class, preventing the use of unsat core when using the optimizer. Despite Optimize.UnsatCore seems to be implemented, without a way to add named assertions, there is no way to obtain the unsat core list without the capability to add named assertions - only empty list is returned.

Since other language bindings, e.g. Python, already have such support, it would be convenient if these methods were available on Optimize as well as Solver in the .NET binding as well.