let display_model c out m = 
  begin
    let constants=Z3.get_model_constants c m in
    let f i e =
      let name = Z3.get_decl_name c e in
      let (ok, v)  = Z3.eval_func_decl c m e in
      display_symbol c out name;
      fprintf out " = ";
      display_ast c out v;
      fprintf out "\n"
    in Array.iteri f constants;
    display_function_interpretations c out m;
  end