let rec merge e s =
  changed := Term.Set.empty;
  let s' = merge1 e s in
    (!changed, s')
    
and merge1 e s =
  Trace.msg "c1" "Merge(c)" e Fact.pp_equal;
  let (x, y, _) = Fact.d_equal e in
    try
      let (i, _) = apply s x in
        (try
           let (j, _) = apply s y in
           let c1 = Fact.mk_cnstrnt y (Sign.inter i j) None in
             update c1 (restrict x s)
         with
             Not_found -> 
               let c1 = Fact.mk_cnstrnt y i None in
                 update c1 (restrict x s))
    with
        Not_found -> s