Thank you, I will report it there. Your suggestion definitely improves the situation, but it is still not perfect, because the arrows are not at the same level vertically, see screenshot below:

However, for my specific case the two operands are the same height vertically (unlike the letters “a” and “b” above), so your suggested solution is acceptable, i.e. the height difference is not too bad:
