let rec sat s p =
  try
    initialize s;
    let result =
      let mode = Jst.Mode.get() != Jst.Mode.No in
        if icsat_sat (to_prop p) mode then
          begin
            debug_output();
            Some(assignment(), top())
          end 
        else 
          None
    in
      if !statistics then
        icsat_print_statistics();
      finalize();
      result
  with
      exc ->
        finalize ();
        raise exc

and debug_output () =
  if debug then
    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 "\nassert ";
           Atom.pp fmt a; 
           Pretty.string fmt ".")
        !bl

        
and assignment () =
  let valuation =
    Name.Hash.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 = 
    Atom.Map.fold
      (fun a id acc ->
          (match icsat_get_assignment id with
             | (-1) -> Atom.Set.add (Atom.negate Arith.mk_neg a) acc  
             | 0 -> acc                      (* don't care *)
             | 1 -> Atom.Set.add a acc       (* true *)
             | _ -> failwith "ICSAT: invalid return value of icsat_get_assignment"))
      !atom_to_id_tbl Atom.Set.empty
  in
    { Assignment.valuation = valuation; Assignment.literals = literals }