In order to get rid of the apparent bug, {ANNOTATED_ARRAYED_SET}.symdif was rewritten as below.

	symdif (other: TRAVERSABLE_SUBSET [G])
			-- <Precursor>
		local
			int: like Current
		do
			int := twin
			int.intersect (other)
			merge (other)
			subtract (int)
		ensure then
			-- As before...
		end

It seems to have defeated the bug.