/*
 * taken from issue #394
 */
int main()
{
  const char *conststring = "42";
  return 1;
}