While working with PR #26 it was discovered that loop invariants where never translated into proper ACSL when the -acsl option is given. Investigation and implementation in the result processing parts (e.g. in ACSLExpressionProcessor) is needed for a more complete ACSL translation support.
