Loop assigns are not taken into account when proving a safety PO (#2360) · Issues · pub / frama-c