Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 192918)
+++ gnat_rm.texi	(working copy)
@@ -105,6 +105,7 @@
 * Pragma Ada_2012::
 * Pragma Annotate::
 * Pragma Assert::
+* Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Ast_Entry::
@@ -843,6 +844,7 @@
 * Pragma Ada_2012::
 * Pragma Annotate::
 * Pragma Assert::
+* Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Ast_Entry::
@@ -1195,7 +1197,23 @@
 of Ada, and the DISABLE policy is an implementation-defined
 addition.
 
+@node Pragma Assert_And_Cut
+@unnumberedsec Pragma Assert_And_Cut
+@findex Assert_And_Cut
+@noindent
+Syntax:
+@smallexample @c ada
+pragma Assert_And_Cut (
+  boolean_EXPRESSION
+  [, string_EXPRESSION]);
+@end smallexample
 
+@noindent
+The effect of this pragma for compilation is exactly the same as the one
+of pragma @code{Assert}. This pragma is used to help formal verification
+tools by marking program points where the tool can simplify precise
+knowledge about execution based on the assertion given.
+
 @node Pragma Assertion_Policy
 @unnumberedsec Pragma Assertion_Policy
 @findex Debug_Policy
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 192918)
+++ sem_prag.adb	(working copy)
@@ -6759,14 +6759,17 @@
             end if;
          end Annotate;
 
-         ------------
-         -- Assert --
-         ------------
+         -----------------------------
+         -- Assert & Assert_And_Cut --
+         -----------------------------
 
          --  pragma Assert ([Check =>] Boolean_EXPRESSION
          --                 [, [Message =>] Static_String_EXPRESSION]);
 
-         when Pragma_Assert => Assert : declare
+         --  pragma Assert_And_Cut ([Check =>] Boolean_EXPRESSION
+         --                         [, [Message =>] Static_String_EXPRESSION]);
+
+         when Pragma_Assert | Pragma_Assert_And_Cut => Assert : declare
             Expr : Node_Id;
             Newa : List_Id;
 
@@ -6784,6 +6787,13 @@
             --  So rewrite pragma in this manner, transfer the message
             --  argument if present, and analyze the result
 
+            --  Pragma Assert_And_Cut is treated exactly like pragma Assert by
+            --  the frontend. Formal verification tools may use it to "cut" the
+            --  paths through the code, to make verification tractable. When
+            --  dealing with a semantically analyzed tree, the information that
+            --  a Check node N corresponds to a source Assert_And_Cut pragma
+            --  can be retrieved from the pragma kind of Original_Node(N).
+
             Expr := Get_Pragma_Arg (Arg1);
             Newa := New_List (
               Make_Pragma_Argument_Association (Loc,
@@ -15185,6 +15195,7 @@
       Pragma_All_Calls_Remote               => -1,
       Pragma_Annotate                       => -1,
       Pragma_Assert                         => -1,
+      Pragma_Assert_And_Cut                 => -1,
       Pragma_Assertion_Policy               =>  0,
       Pragma_Assume_No_Invalid_Values       =>  0,
       Pragma_Asynchronous                   => -1,
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 192918)
+++ par-prag.adb	(working copy)
@@ -1098,6 +1098,7 @@
            Pragma_All_Calls_Remote               |
            Pragma_Annotate                       |
            Pragma_Assert                         |
+           Pragma_Assert_And_Cut                 |
            Pragma_Asynchronous                   |
            Pragma_Atomic                         |
            Pragma_Atomic_Components              |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 192918)
+++ snames.ads-tmpl	(working copy)
@@ -448,6 +448,7 @@
    --  correctly recognize and process Name_AST_Entry.
 
    Name_Assert                         : constant Name_Id := N + $; -- Ada 05
+   Name_Assert_And_Cut                 : constant Name_Id := N + $; -- GNAT
    Name_Asynchronous                   : constant Name_Id := N + $;
    Name_Atomic                         : constant Name_Id := N + $;
    Name_Atomic_Components              : constant Name_Id := N + $;
@@ -1697,6 +1698,7 @@
       Pragma_Abort_Defer,
       Pragma_All_Calls_Remote,
       Pragma_Assert,
+      Pragma_Assert_And_Cut,
       Pragma_Asynchronous,
       Pragma_Atomic,
       Pragma_Atomic_Components,