let rec atom s =
    Trace.func "process" "Process" Atom.pp (Status.pp pp)
      (fun a ->
         try
           (match Can.atom s a with
              | Atom.True -> 
                  Status.Valid
              | Atom.False ->
                  Status.Inconsistent
              | a ->
                  Status.Ok(protect
                              (fun s ->
                                 s.ctxt <- Atom.Set.add a s.ctxt;
                                 let (s, a) = Abstract.atom (s, a) in
                                   process a s)
                              s))
         with 
             Exc.Inconsistent -> 
               Status.Inconsistent)

  and process a s = 
    match a with
      | Atom.Equal(x, y) ->
          let e = Fact.mk_equal x y Fact.mk_axiom in
            normalize (equality e s)
      | Atom.Diseq(x, y) ->
          let d = Fact.mk_diseq x y Fact.mk_axiom in
            normalize (diseq d s)
      | Atom.In(x, d) ->
          let c = Fact.mk_cnstrnt x d Fact.mk_axiom in
            normalize (add c s)
      | Atom.True -> 
          s
      | Atom.False ->
          raise Exc.Inconsistent
             
  and protect f s =
   let k' = !Var.k in
     try
       Var.k := s.upper;
       let s' = f (copy s) in
         s'.upper <- !Var.k;
         Var.k := k';
         s'
     with
       | exc ->
           Var.k := k';
           raise exc