1 files changed, 10 insertions, 0 deletions
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 9138442..443c6ff 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -3532,6 +3532,16 @@ package body Exp_Ch7 is
       elsif Nkind (Wrap_Node) = N_Iteration_Scheme then
          null;
 
+      --  In formal verification mode, if the node to wrap is a pragma check,
+      --  this node and enclosed expression are not expanded, so do not apply
+      --  any transformations here.
+
+      elsif ALFA_Mode
+        and then Nkind (Wrap_Node) = N_Pragma
+        and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
+      then
+         null;
+
       else
          Push_Scope (New_Internal_Entity (E_Block, Current_Scope, Loc, 'B'));
          Set_Scope_Is_Transient;