let rec split s =
  Atom.Set.union 
    (split_cnstrnt s) 
    (split_arrays s)

and split_cnstrnt s = 
  (* C.split (c_of s) *)
  Atom.Set.empty

and split_arrays s = 
  Solution.fold
    (fun _ (b,_) acc1 ->
       match b with
         | App(Arrays(Select), [upd1; j1]) ->
             V.fold (v_of s)
             (fun upd2 acc2 ->
                try
                  (match apply arr s upd2 with
                     | App(Arrays(Update), [_; i2; _]) ->
                         (match is_equal s i2 j1 with
                            | X -> Atom.Set.add (Atom.mk_equal (i2, j1)) acc2
                            | _ -> acc2)
                     | _ -> 
                         acc1)
                with
                    Not_found -> acc1)
             upd1 acc1
         | _ -> acc1)
    (eqs_of s arr)
    Atom.Set.empty