diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c661a3832ddf..99b551f1d0cb 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-08-14  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch4.adb (Expand_N_Quantified_Expression): Freeze
+	explicitly the type of the loop parameter.
+
 2019-08-14  Javier Miranda  <miranda@adacore.com>
 
 	* sem_util.adb (New_Copy_Tree.Copy_Node_With_Replacement):
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 4404c5dca9da..00f9aae51a3e 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -10337,8 +10337,30 @@ package body Exp_Ch4 is
       Flag      : Entity_Id;
       Scheme    : Node_Id;
       Stmts     : List_Id;
+      Var       : Entity_Id;
 
    begin
+      --  Ensure that the bound variable is properly frozen. We must do
+      --  this before expansion because the expression is about to be
+      --  converted into a loop, and resulting freeze nodes may end up
+      --  in the wrong place in the tree.
+
+      if Present (Iter_Spec) then
+         Var := Defining_Identifier (Iter_Spec);
+      else
+         Var := Defining_Identifier (Loop_Spec);
+      end if;
+
+      declare
+         P : Node_Id := Parent (N);
+      begin
+         while Nkind (P) in N_Subexpr loop
+            P := Parent (P);
+         end loop;
+
+         Freeze_Before (P, Etype (Var));
+      end;
+
       --  Create the declaration of the flag which tracks the status of the
       --  quantified expression. Generate:
 
diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index 6b71b95ba3a5..9923987ec42d 100644
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2019-08-14  Ed Schonberg  <schonberg@adacore.com>
+
+	* gnat.dg/assert2.adb, gnat.dg/assert2.ads: New testcase.
+
 2019-08-14  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* gnat.dg/inline18.adb, gnat.dg/inline18.ads,
diff --git a/gcc/testsuite/gnat.dg/assert2.adb b/gcc/testsuite/gnat.dg/assert2.adb
new file mode 100644
index 000000000000..1328004ec758
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/assert2.adb
@@ -0,0 +1,5 @@
+--  { dg-do compile }
+
+package body Assert2 is
+   procedure Dummy is null;
+end Assert2;
diff --git a/gcc/testsuite/gnat.dg/assert2.ads b/gcc/testsuite/gnat.dg/assert2.ads
new file mode 100644
index 000000000000..adf9b9212182
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/assert2.ads
@@ -0,0 +1,15 @@
+package Assert2
+    with SPARK_Mode
+is
+   type Living is new Integer;
+   function Is_Martian (Unused : Living) return Boolean is (False);
+
+   function Is_Green (Unused : Living) return Boolean is (True);
+
+   pragma Assert
+     (for all M in Living => (if Is_Martian (M) then Is_Green (M)));
+   pragma Assert
+     (for all M in Living => (if Is_Martian (M) then not Is_Green (M)));
+
+   procedure Dummy;
+end Assert2;