BugFix to allow compilation with gcc 7.1

Propagating the fix in !830 (merged) into 2017-patches. As discussed, this is fixes a bug spotted by gcc7, relevant also for non-gcc7 compilations