How to get all solutions from a theorem?

[LittleLittleCloud]

e.g. input theorem

using (var ctx = new Z3Context())
{
    var theorem = from t in ctx.NewTheorem<(bool x, bool y)>()
                  where t.x ^ t.y
                  select t;
}

output

(true, false) (false, true)

[idg10]

Although we maintain this library, I don't actually have in depth knowledge of Z3, so I'm not entirely sure whether this is a feature available in Z3 that we can surface.

But I note that this: https://brandonrozek.com/blog/obtaining-multiple-solutions-z3/ shows that with the Python wrapper for Z3, the way to do it is to introduce the results of earlier solutions as additional constraints. (So whether or not Z3 has a built-in feature to do this, the Python Z3 wrapper exposes no such functionality.)

So as I understand it, the process is to ask Z3 for a solution, and then to essentially add a constraint saying "But not this particular solution please", and then ask it to solve that. And you keep going until it's unable to find a solution.

Is that something that could work in your scenario?