When adding a formula to a context, instead of creating e new prover and checking the and, just put the formula in the context and if it becomes unsat, retract it (incremental building the formula). See for instance:
https://stackoverflow.com/questions/16422018/how-incremental-solving-works-in-z3?rq=1