[Ada] Crash on precondition involving quantified expression

--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -20799,16 +20799,27 @@  package body Sem_Util is
          --  this restriction leads to a performance penalty.
 
          --  ??? this list is flaky, and may hide dormant bugs
+         --  Should functions be included???
+
+         --  Loop parameters appear within quantified expressions and contain
+         --  an entity declaration that must be replaced when the expander is
+         --  active if the expression has been preanalyzed or analyzed.
 
          elsif not Ekind_In (Id, E_Block,
                                  E_Constant,
                                  E_Label,
+                                 E_Loop_Parameter,
                                  E_Procedure,
                                  E_Variable)
            and then not Is_Type (Id)
          then
             return;
 
+         elsif Ekind (Id) = E_Loop_Parameter
+           and then No (Etype (Condition (Parent (Parent (Id)))))
+         then
+            return;
+
          --  Nothing to do when the entity was already visited
 
          elsif NCT_Tables_In_Use
@@ -21081,7 +21092,14 @@  package body Sem_Util is
       begin
          pragma Assert (Nkind (N) not in N_Entity);
 
-         if Nkind (N) = N_Expression_With_Actions then
+         --  If the node is a quantified expression and expander is active,
+         --  it contains an implicit declaration that may require a new entity
+         --  when the condition has already been (pre)analyzed.
+
+         if Nkind (N) = N_Expression_With_Actions
+           or else
+             (Nkind (N) = N_Quantified_Expression and then Expander_Active)
+         then
             EWA_Level := EWA_Level + 1;
 
          elsif EWA_Level > 0
@@ -21225,6 +21243,12 @@  package body Sem_Util is
       --    * Semantic fields of nodes such as First_Real_Statement must be
       --      updated to reference the proper replicated nodes.
 
+      --  Finally, quantified expressions contain an implicit delaration for
+      --  the bound variable. Given that quantified expressions appearing
+      --  in contracts are copied to create pragmas and eventually checking
+      --  procedures, a new bound variable must be created for each copy, to
+      --  prevent multiple declarations of the same symbol.
+
       --  To meet all these demands, routine New_Copy_Tree is split into two
       --  phases.
 

--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/predicate12.adb
@@ -0,0 +1,6 @@ 
+--  { dg-do compile }
+--  { dg-options "-gnata" }
+
+package body Predicate12 is
+   procedure Dummy is null;
+end Predicate12;

--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/predicate12.ads
@@ -0,0 +1,42 @@ 
+package Predicate12 is
+
+   subtype Index_Type is Positive range 1 .. 100;
+   type Array_Type is array(Index_Type) of Integer;
+
+   type Search_Engine is interface;
+
+   procedure Search
+     (S           : in  Search_Engine;
+      Search_Item : in  Integer;
+      Items       : in  Array_Type;
+      Found       : out Boolean;
+      Result      : out Index_Type) is abstract
+     with
+       Pre'Class =>
+         (for all J in Items'Range =>
+           (for all K in J + 1 .. Items'Last => Items(J) <= Items(K))),
+       Post'Class =>
+         (if Found then Search_Item = Items(Result)
+                   else (for all J in Items'Range => Items(J) /= Search_Item));
+
+   type Binary_Search_Engine is new Search_Engine with null record;
+
+   procedure Search
+     (S           : in  Binary_Search_Engine;
+      Search_Item : in  Integer;
+      Items       : in  Array_Type;
+      Found       : out Boolean;
+      Result      : out Index_Type) is null;
+
+   type Forward_Search_Engine is new Search_Engine with null record;
+
+   procedure Search
+     (S           : in  Forward_Search_Engine;
+      Search_Item : in  Integer;
+      Items       : in  Array_Type;
+      Found       : out Boolean;
+      Result      : out Index_Type) is null;
+
+   procedure Dummy;
+
+end Predicate12;