-@code{verify (@var{EXPRESSION});} is a declaration; it can occur
-outside of functions. In contrast, @code{verify_true
-(@var{EXPRESSION})} is an integer constant expression that always
-evaluates to 1; it can be used in macros that expand to
-expressions.
-
-@var{EXPRESSION} should be an integer constant expression in the sense
+@code{verify (@var{V});} is a declaration; it can occur outside of
+functions. In contrast, @code{verify_expr (@var{V}, @var{EXPR})} is
+an expression that returns the value of @var{EXPR}; it can be used in
+macros that expand to expressions. If @var{EXPR} is an integer
+constant expression, then @code{verify_expr (@var{V}, @var{EXPR})} is
+also an integer constant expression. Although @var{EXPR} and
+@code{verify_expr (@var{V}, @var{EXPR})}@ are guaranteed to have the
+same side effects and value and type (after integer promotion), they
+need not have the same type if @var{EXPR}'s type is an integer that is
+narrower than @code{int} or @code{unsigned int}.
+
+@var{V} should be an integer constant expression in the sense