let rec sat s p =
  try
    init s;
    let result = 
      if icsat_sat (to_prop p) then
        begin
          debug();
          Some(assignment (), top())
        end 
      else 
        None
    in
      if !statistics then
        icsat_print_statistics();
      finalize();
      result
  with
      exc ->
        finalize ();
        raise exc

and debug () =
  let fmt = Format.std_formatter in
  let bl = ref [] in
    Stack.iter
      (fun (s, al) -> bl := (List.rev al) @ !bl)    
      stack;
    List.iter 
      (fun a -> 
         Pretty.string fmt "assert ";
         Atom.pp fmt a; 
         Pretty.string fmt ".\n")
      !bl

        
and assignment () =
  let valuation =
    Nametbl.fold
      (fun x id acc ->
         match icsat_get_assignment id with
           | (-1) -> (x, false) :: acc
           | 0 -> acc                   (* don't care *)
           | 1 -> (x, true) :: acc       
           | _ -> failwith "ICSAT: invalid return value of icsat_get_assignment")
      vartbl []
  in
  let literals = 
    Atomtbl.fold
      (fun a id acc ->
         Trace.msg "foo5" "Atom" (id, a) (Pretty.pair Pretty.number Atom.pp);
          (match icsat_get_assignment id with
             | (-1) -> Atom.negate a :: acc  
             | 0 -> acc               (* don't care *)
             | 1 -> a :: acc          (* true *)
             | _ -> failwith "ICSAT: invalid return value of icsat_get_assignment"))
      idtbl []
  in
    { Assignment.valuation = valuation; Assignment.literals = literals }