If an annotation contains an existential, the resulting constraint is not CHC and cannot be solved by Spacer. We use PCSat for that kind of example in tests via environment variables, but it would be convenient to switch solver from within source code.
If an annotation contains an existential, the resulting constraint is not CHC and cannot be solved by Spacer. We use PCSat for that kind of example in tests via environment variables, but it would be convenient to switch solver from within source code.