With the recent addition of UserPropagators, I'm wondering if the solver is able to safely support more than one in the same context?
Turns out this isn't supported, based on the discussion here: https://github.com/Z3Prover/z3/discussions/6382