+The @file{verify.h} header defines one more macro, @code{assume
+(@var{E})}, which expands to an expression of type @code{void}
+that causes the compiler to assume that @var{E} yields a nonzero
+value. @var{E} should be a scalar expression, and should not
+have side effects; it may or may not be evaluated. The behavior is
+undefined if @var{E} would yield zero. The main use of @code{assume}
+is optimization, as the compiler may be able to generate better code
+if it assumes @var{E}. For best results, @var{E} should be simple
+enough that a compiler can determine that it has no side effects: if
+@var{E} calls an external function or accesses volatile storage the
+compiler may not be able to optimize @var{E} away and @code{assume
+(@var{E})} may therefore slow down the program.
+
+Here are some example uses of these macros.