PR# 19652 Postcondition violation in SPECIAL.copy

The implementation of SPECIAL.copy violates its postcondition "is_equal":

		local
			sp1, sp2: SPECIAL [CHARACTER]
		do
				-- `sp1' has more items than `sp2'.
				-- All items of `sp2' will be copied to `sp1'.
				-- The other items in `sp1' will not be changed.
				-- The 'count' and 'capacity' in `sp1' will not change.
			create sp1.make_empty (10)
			sp1.extend ('a')
			sp1.extend ('b')
			sp1.extend ('c')
			create sp2.make_empty (5)
			sp2.extend ('x')
			sp2.extend ('y')
			sp1.copy (sp2)

--
Eric Bezault