| [] ->
m, B.Bind (a, B.Abst (true, n, w), t), None
| (c, v) :: s ->
| [] ->
m, B.Bind (a, B.Abst (true, n, w), t), None
| (c, v) :: s ->
if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
let v = B.Cast (E.empty_node, w, v) in
let e = B.push m.e c a (B.abbr v) in
if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
let v = B.Cast (E.empty_node, w, v) in
let e = B.push m.e c a (B.abbr v) in
if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
| B.GRef ({E.n_apix = e1}, u1), Some v1,
B.GRef ({E.n_apix = e2}, u2), Some v2 ->
if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
| B.GRef ({E.n_apix = e1}, u1), Some v1,
B.GRef ({E.n_apix = e2}, u2), Some v2 ->
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)
end else if e2 < e1 then begin
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, t2, r2)
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)
end else if e2 < e1 then begin
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, t2, r2)
| _, _, B.GRef _, Some v2 ->
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)
| _, _, B.GRef _, Some v2 ->
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)