Use uninterpreted function symbols in Z3 IR translator for unknown pure ops

Currently, whenever we translate an op that we haven't implemented translation for, we turn it into a fresh variable. In the case of effectful unimplemented ops, this is the best we can do, but if the op is not effectful we can turn it into an uninterpreted function symbol applied to each of its operands (translated). Adding UF symbols does potentially negatively impact the runtime (it turns the theory from `QF_BV` to `QF_UFBV` in Z3 parlance), but I think it's probably worthwhile.