copy from ex4.elf
wip on alternative proof for test9 without using restrict-sub-tp, just like test12z