let nb_diff a1 a2 =
TimerSubset.start ();
let cpt = ref 0 in
let n1 = Array.length a1 in
let n2 = Array.length a2 in
let i1 = ref 0 in
let i2 = ref 0 in
while !i1 < n1 && !i2 < n2 do
let c = Atom.compare a1.(!i1) a2.(!i2) in
if c = 0 then (incr i1; incr i2)
else if c < 0 then (incr cpt; incr i1)
else incr i2
done;
TimerSubset.pause ();
!cpt + (n1 - !i1)