| [] ->
m, B.Bind (a, B.Abst (true, n, w), t), None
| (c, v) :: s ->
-(*
- if !G.cc && not (N.assert_not_zero st n) then assert false;
-*)
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 e1 < e2 then begin
+ if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
+ else if e1 < e2 then begin
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)
- end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
- else begin
+ end else begin
if !G.summary then O.add ~gdelta:2 ();
ac st m1 v1 m2 v2
- end
+ end
| _, _, B.GRef _, Some v2 ->
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)