let merge e s = 
  Trace.msg "p" "Merge" e Fact.pp_equal;
  let (x, y, _) = Fact.d_equal e in
    match is_equal s x y with
      | Three.Yes -> 
          (nochange, s)
      | Three.No -> 
          raise Exc.Inconsistent
      | Three.X ->
          let (chv', v') = V.merge e s.v
          and (chd', d') = D.merge e s.d
          and (chc', c') = C.merge e s.c in
          let ch' = {chv = chv'; chd  = chd'; chc = chc'} in
          let s' = update_c (update_v (update_d s d') v') c' in
            (ch', s')