[E-ACSL] my previous tentative patch did not work. I prefer to have E-ACSL that works than non-regression tests...