diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9fc8c9e1139..9222a98150d 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-08-19  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Resolve_Call): Check non-aliasing rules before
+	GNATprove inlining.
+
 2019-08-19  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* inline.adb (Add_Inlined_Body): Do not add pending
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index b27171f0be5..8f2e35894d4 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6968,6 +6968,10 @@ package body Sem_Res is
 
       Build_Call_Marker (N);
 
+      Mark_Use_Clauses (Subp);
+
+      Warn_On_Overlapping_Actuals (Nam, N);
+
       --  In GNATprove mode, expansion is disabled, but we want to inline some
       --  subprograms to facilitate formal verification. Indirect calls through
       --  a subprogram type or within a generic cannot be inlined. Inlining is
@@ -7116,10 +7120,6 @@ package body Sem_Res is
             end if;
          end if;
       end if;
-
-      Mark_Use_Clauses (Subp);
-
-      Warn_On_Overlapping_Actuals (Nam, N);
    end Resolve_Call;
 
    -----------------------------