In Z3, soft constraints can be implemented by placing the actual constraint P on the right-hand side of an implication whose left-hand side is a fresh boolean variable, e.g. assert (=> b1 P). Constraints can then be "switched on" per check-sat by listing bs which are to be considered true, e.g. (check-sat b1).
Question: What happens with such constraints P if their guard variable b is not included in a check-sat? I assume Z3 treats b's value as unknown, and then branches over the implication/over b's value - is that correct?
Background: The background of my question is that I use Z3 in incremental mode (push/pop blocks), and that I check assertions P by (push)(assert (not P))(check-sat)(pop); if the check-sat is unsat then P holds.
I thought about using soft constraints instead, i.e. to replace each such push/pop block by (declare-const b_i Int)(assert (=> b_i P))(check-sat b_i). Each b_i would only be used once. However, if Z3 may branch over all previous b_j, then it sounds as if that might potentially slow down Z3 quite a bit - hence my question.
(P.S.: I am aware of this answer by Leo, which says that soft constraints might also reduce performance because certain optimisations might not be applicable.)
