#include<stdio.h>
#include<stdlib.h>

int main(int argc, char * argv[]) {
	printf("%.15f\n", 12345.678910111213);
	/* le format est arrondi à la 12eme décimale.
	Essayer d'en print plus donne des nombres incohérents */
  	return EXIT_SUCCESS;
}