Continue SPARK-Ada translation; fix three bugs in IDIOM 7 suppression; fix iterator error that can cause an infinite loop.
