returned to Lihao's primitive bug, we have to wait for CBMC treating struct fields as individual shared variables
extended logger added