See http://stackoverflow.com/questions/16839658 -- although
in most cases 16 decimal digits suffices for a double
precision value, in a handful of instances 17 are necessary.
At the command line, see the difference between:

$ printf %.17g 1.0000000000000001

and

$ printf %.16g 1.0000000000000001

Since SPINS does not provide bit-for-bit compatibility when
restarting (because of the startup timestepping approach),
this change is unlikely to make any significant difference
to existing or future cases.