let rec add c s =  
  Trace.msg "c1" "Add" c Fact.pp_cnstrnt;
  changed := Term.Set.empty;
  let s' = update c s in
    (!changed, s')