Multiple UserPropagators Example

[JoanEspasa]

Hello everyone,

I wanted to ask if two or more UserPropagators [1] can be combined with the same solver. I'm doing something like this in Python:

s = SimpleSolver()
for x in xs:
    s.add(x % 2 == 1)
p = UserPropagate1(s)
p = UserPropagate2(s)
s.check()
print(s.model())

but even if the UserPropagate2 class does not bind to anything (i.e., it does nothing) I get a Segmentation Fault on the python interpreter. I'm using version 4.11.2 - 64bit.

More generally, I'm wondering if that is conceptually possible considering how UserPropagators are implemented in Z3, and if that is the case, how it behaves when two propagators bind to the same variables.

Many thanks in advance!

[1] https://microsoft.github.io/z3guide/programming/Example%20Programs/User%20Propagator

[NikolajBjorner]

This isn't supported. Never tested and the internals don't let you re-register a propagator.
It shouldn't crash, but that is a bug in the error path.
You register a single user propagator. If you need two different functionalities you are responsible for tee-ing.
There is a function for registering a function declaration. It assumes a single propagator. So changing it to teeing the propagator internally isn't straight-forward.

[JoanEspasa]

Many thanks Nikolaj for the speedy reply!