let add c s =
  Trace.msg "p" "Add" c Fact.pp_cnstrnt;
  let (chc', c') = C.add c s.c in
  let ch' = {nochange with chc = chc'} in
  let s' = update_c s c' in
    (ch',  s')