F-c OK - the problem seems to be the difference when new_head is modeled using Hoare mem model and when memory is taken (for example assert finite(&new_head);) it switches to different mode