MCSAT UF Plugin performance bugs #662

There are two bugs in the uf plugin of mcsat:

• The uf plugin's pop discarded the e-graph evaluations of re-added equality terms, even though their trail values had just been popped. The solver could then decide such an equality against its e-graph value, recreating the same conflict until a restart. This leads to a termination issue in tests/regress/both/wd_issue294.smt2 which is only solved by a restart.
• Function eq_graph_merge_preference does the opposite of the claimed operation. It leads to merging the bigger into the smaller set.