#include <stdio.h>
int main(int argc, char **argv) {
  float Realvar;
  Realvar = 1.25e7;
  fprintf(stderr, "%d\n", *(int *)&Realvar);
  return (0);
}