In particular, Bitwuzla appears to normalize upto commutativity, as well as exploiting properties such as NaN propagation and injectivity of negation.