let rec display_ast c out v =
  begin
    match Z3.term_refine c v with
    | Z3.Term_app(k, f, args) -> 
      let num_fields = Array.length args in
      let a = Z3.to_app c v in
      let d = Z3.get_app_decl c a in
      Printf.fprintf out "%s" (Z3.func_decl_to_string c d);
      if num_fields > 0 then 
         begin
           Printf.fprintf out "[";
           for i = 0 to num_fields - 1 do
               if i > 0 then Printf.fprintf out ", ";
                display_ast c out (Z3.get_app_arg c a i)
           done;
           Printf.fprintf out "]"
         end
    | Z3.Term_numeral(nm, s) -> 
      display_numeral c out nm;
      Printf.fprintf out ":";
      display_sort c out s 
    | Z3.Term_var(idx, s) -> ()
    | Z3.Term_quantifier(b, w, pats, bound, body) -> ()
  end