starting from <fibonacci>
rdi := nondet as n
assume 0 <= n <= 10
reach* <fibonacci> return then print dec rax
cut at <fibonacci> return