Update changelog.
Fix a bug in the stratification algorithm.

The previous coding was wrong -- in some cases, a cycle through negation was not
detected correctly. This meant that some unstratifiable programs were not
rejected (and instead we might produce incorrect results for them).

Along the way, do some minor code cleanup.