Z3 does not support this directly through the .NET API. Instead, a Boolean constant should be created (the name, e.g., x
), which can then be used to assert conditional constraints, e.g.,
solver.AssertAndTrack(constraint, x);
The constraint is then named x
and this constant is used to refer to it in the unsat cores.
For an example in Python, see also this other question; the strategy is the same in the .NET API, only the function names differ slightly.