Loop invariants and a constraint relaxation are used to solve this problem.

divisible_by_three.pdf