The rationale for this change is that the major case of term duplication
is a transformation that changes only some parts of a term, leaving the
rest intact. This case can be handled with the help of Term.t_label_copy
(which must be called anyway, to preserve labels): if the two terms are
"similar", i.e. composed from the identical components, we return the
original and drop the copy. The duplication of unrelated terms is more
rare, because of bound variables which are mostly unique.

Decls and tasks are still h-consed, however, to permit memoization.

On the same example of BWare the gain is quite visible:

why3-replayer : hcons

242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k

why3-replayer : no hcons

106.81user 7.86system 1:59.32elapsed 96%CPU (0avgtext+0avgdata 1656908maxresident)k