const char* filename_pattern = "./GiNaCXXXXXX";
char* new_filename = new char[strlen(filename_pattern)+1];
strcpy(new_filename, filename_pattern);
const char* filename_pattern = "./GiNaCXXXXXX";
char* new_filename = new char[strlen(filename_pattern)+1];
strcpy(new_filename, filename_pattern);