Suppose one has a model $M$$\vDash$$NGBC^{-f}$+BAFA. Does there exist a (class) forcing extension $M[G]$$\vDash$$NGBC^{-f}$+$BAFA$ that has a submodel $N$$\vDash$$NGB^{-f}$+$BAFA$+$\lnot$$AC$? Can one also construct permutation models of $NGB^{-f}$+$BAFA$+$\lnot$$AC$?
Note $NGB^{-f}$ is von Neumann-Goedel-Bernays set theory without the axiom of foundation.
$BAFA$ is Boffa's Anti-Foundation Axiom; that is, that
"...for every transitive set $t_0$ and every extensional binary relation $<$$a$,$e$$>$ that end-extends $<$$t_0$, $\in$$>$, meaning $t_0$$\subseteq$$a$ and $\in$$\upharpoonright$$t_0$=$e$$\cap$($a$$\times$$t_0$), there exists a transitive set $t$, and an isomorphism from $<$$a$,$e$$>$ to $<$$t$,$\in$$>$ that is the identity on $t_0$..."
(this from Daghighi's, Golshani's, Hamkins',and Jerabek's preprint "The Role of the Foundation Axiom in the Kunen Inconsistency", from which the notation was taken and the motivation for this question.)