BTW, 1.2 and 12.0 are directly representable as double
In C++:
printf("%.20f\r\n", 1.2);
printf("%.20f\r\n", 12.0);
will output:
1.20000000000000000000
12.00000000000000000000
Either upcasting to real is the wrong decision here, either the
writeln string conversion is wrong.
