+ --
+ -- NB: We do *not* go around for new extra_eqs. Morally, we should,
+ -- but we can't without risking non-termination (see #2688). By
+ -- not going around, we miss some legal programs mixing FDs and
+ -- TFs, but we never claimed to support such programs in the
+ -- current implementation anyway.