Consequences of foundation/regularity in ordinary mathematics (over ZF–AF)?

It has long been the informal view of set theorists that the Axiom of Foundation does not have consequences for "ordinary mathematics". For example, in Chapter III of his Set Theory: An Introduction to Independence Proofs (1980), K. Kunen tells us that we introduce the axiom to limit set theory to the sets that are actually employed to do mathematics. Similarly, in their mathematico-philosophical classic Foundations of Set Theory (1973, p. 87)), A. A. Fraenkel, Y. Bar-Hillel and A. Levy maintain "its omission will not incapacitate any field of mathematics". Of course mathematics has changed since these works were written, but I suspect the opinions expressed therein have not changed among contemporary set theorists with respect to what you informally call "ordinary mathematics".

What about Scott's trick?

In more detail: here, I claim, is a proof-schema in ZF that belongs to "ordinary mathematics" but cannot be trivially modified to go through in ZF–AF.

Let $C$ be a locally-large category, by which I mean a proper class of objects, a proper class of morphisms, class-functions for domain, codomain, composition, and identities, satisfying the axioms of a category. (Since a proper class in ZF is specified by a logical formula, this is why the proof is a schema rather than a single one.) Let $W$ be a subclass of the morphisms of $C$. Then we can construct the localization $C[W^{-1}]$ as another locally-large category, as described here: we consider the (large) directed graph whose edges are the morphisms of $C$ and the morphisms of $W^{\rm op}$, generate the free (large) category on it, and then quotient by an appropriate equivalence relation.

The free large category on a large directed graph is unproblematic even in ZF–AF: its morphisms are finite lists of composable edges, and we can define a formula that specifies the proper class of finite sequences of elements of some other proper class. But there is no obvious way to form the quotient of a generic proper class by a proper-class equivalence relation in ZF–AF: the usual construction of the quotient of a set by an equivalence relation takes the elements of the quotient to be equivalence classes, but if the "equivalence classes" are proper classes then they cannot be elements of some other class. Scott's trick is to instead define the elements of the quotient to be the sub-sets of the equivalence proper-classes consisting of all their elements of minimal rank, which are sets since each $V_\kappa$ is a set. But without the axiom of foundation, this doesn't work since we can't assert that each equivalence proper-class contains any well-founded elements.