let to_prop p =
  let rec translate rho p =
    match p with
      | True -> 
          icsat_mk_true()
      | False -> 
          icsat_mk_false()
      | Var(x) -> 
          (try
             let q = List.assoc x rho in
               translate rho q
           with
               Not_found -> 
                 let id = icsat_mk_var (Name.to_string x) in
                   if not(Nametbl.mem vartbl x) then
                     Nametbl.add vartbl x id;
                   id)
      | Atom(a) -> 
          assert(Atom.is_negatable a);
          let b = Atom.negate a in
          let i = atom_to_id a in
          let j = atom_to_id b in
          let id = icsat_mk_atom i j in
            Trace.msg "foo6" "Idtbl.add" (a, id) (Pretty.pair Atom.pp Pretty.number);
            if not(Atomtbl.mem idtbl a) then
              Atomtbl.add idtbl a id;
            id
      | Let(x, p, q) ->
          (match p with
             | Var _ ->
                 raise (Invalid_argument "No variable definitions")
             | _ ->
                 translate ((x, p) :: rho) q)
      | Disj(pl) ->
          icsat_mk_or (List.map (translate rho) pl)
      | Iff(p, q) ->
          icsat_mk_iff (translate rho p) (translate rho q)
      | Ite(p, q, r) ->
          icsat_mk_ite (translate rho p) (translate rho q) (translate rho r)
      | Neg(p) ->
          icsat_mk_not (translate rho p)
  in
    translate [] p