let rec display_sort c out ty =
  begin
    match Z3.sort_refine c ty with 
    | Z3.Sort_uninterpreted s -> display_symbol c out s;
    | Z3.Sort_bool -> fprintf out "bool";
    | Z3.Sort_int -> fprintf out "int";
    | Z3.Sort_real -> fprintf out "real";
    | Z3.Sort_bv sz -> fprintf out "bv%d" sz;
    | Z3.Sort_array (domain, range) ->
      fprintf out "[";
      display_sort c out domain;
      fprintf out "->";
      display_sort c out range;
      fprintf out "]";
    | Z3.Sort_datatype cons ->
      Array.iter (fun (dt_con : Z3.datatype_constructor_refined) -> 
       let fields = dt_con.Z3.accessors in
       fprintf out "(";
       let f i v = 
         if i>0 then fprintf out ", ";
         display_sort c out (Z3.get_range c v);
       in Array.iteri f fields;
       fprintf out ")") cons
    | Z3.Sort_unknown s ->
      fprintf out "unknown[";
      display_symbol c out s;
      fprintf out "unknown]";
  end