The backend for formal verification handles much more easily aggregates that are not expanded into loops, as this happens with array aggregates, so prevent expansion in this mode.
Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-29 Yannick Moy <m...@adacore.com> * exp_aggr.adb (Expand_Array_Aggregate): Do not expand array aggregates in formal verification.
Index: exp_aggr.adb =================================================================== --- exp_aggr.adb (revision 178155) +++ exp_aggr.adb (working copy) @@ -4664,6 +4664,12 @@ Check_Same_Aggr_Bounds (N, 1); end if; + -- In formal verification mode, leave the aggregate non-expanded + + if ALFA_Mode then + return; + end if; + -- STEP 2 -- Here we test for is packed array aggregate that we can handle at