Fix c_rodata optimisation idea.

Experiment with side-proving rodata ineqs.

The suspicion was that some slow-down seen lately was because the
rodata-witness value might now have a disjunction of possible
reasons for difference, which might make the solver logic for
understanding that function input are valid more obscure. A possible
fix for that is to pre-test and pre-assert that the witness must be
disjoint from problem pointers on the C side, based just on their PC.
That should simplify the SMT logic, one might think.