Currently, every rewrite step (except objective function pre-compositions) results in an application of a (custom) congruence rule. This is unnecessary. All the rewrites on a given component can be applied together.
Before: (rewrite_constraint_2; rw_x), (rewrite_constraint_2; rw_y), (rewrite_constraint_2; rw_z), ...
After: rewrite_constraint_2; (rw_x; rw_y; rw_z), ...