Trying to fix a false-positive due to incorrect inductive termination check in 'int' when K is more than 1 (not fixed yet).