It seemed to me too that this particular piece of code should be already present in the symbolic backend, but in fact it's not. The symbolic backend filters the rule condition and appends a call to checkSat, which verifies whether the (path condition /\ filtered rule condition) is NOT unsat. This is equivalent with detecting if the next possible program state is feasible.
On the other hand, here we construct  a different argument for checkSat which checks a logical implication (we want the argument (formula) sent to checkSat TO BE unsat) and we also add some predicates in the rule's side condition. Technically speaking, in two different places we build two different side conditions for rules. The common part is the replacement of the rule's condition, which I think it's easier to be done using rule.setRequires(newCondition) than creating a new Transformer for this.
If you think the above explanation is not ok, then we can go into deeper the details of this.