00181.c:101:[eva] warning: Using specification of function Hanoi for recursive calls.
Analysis of function Hanoi is thus incomplete and its soundness
relies on the written specification.
00181.c:103:[eva] warning: Using specification of function Hanoi for recursive calls.
Analysis of function Hanoi is thus incomplete and its soundness
relies on the written specification.