Dear all :
Please notice that induction-based algorithm should be accompanied with BMC
in your implementation, or your program can never prove property true.
(This TODO is not apparent in the PA spec.)
Any question, please feel free to contact with me and Ric.
Good Luck!