starting from <fibonacci>
rdi := nondet as n
assume 0 <= n <= 10
at 0x400089 assert !of
cut at <fibonacci> return
explore all