// kani-flags: --enable-unstable --cbmc-args --unwind 4 --object-bits 9