let display_function_interpretations c out m =
  begin
    fprintf out "function interpretations:\n";
    let display_function (name, entries, func_else) =
      begin
        display_symbol c out name;
        fprintf out " = {";
        let display_entry j (args,valu) =
          if j > 0 then fprintf out ", ";
          fprintf out "(";
          let f k arg =
            if k > 0 then fprintf out ", ";
            display_ast c out arg
          in Array.iteri f args;
          fprintf out "|->";
          display_ast c out valu;
          fprintf out ")";
        in Array.iteri display_entry entries;
        if Array.length entries > 0 then fprintf out ", ";
        fprintf out "(else|->";
        display_ast c out func_else;
        fprintf out ")}\n";
      end;
    in
    Array.iter display_function (Z3.get_model_funcs c m);
  end