When I try to use push and pop operations for backtracking on z3's fixedpoint solver via python api, "operation is not supported by engine" exception is thrown by the solver.
b = Bool('b')
a = Bool('a')
s = Fixedpoint()
s.register_relation(a.decl())
s.register_relation(b.decl())
s.fact(a)
s.push()
s.rule(b, a)
s.query(b)
s.pop()
Are the push and pop operations are not supported by z3py on the fixedpoint solver?