diff --git a/source/lib-intro.tex b/source/lib-intro.tex
index 2958545e4a..ef791fbdf0 100644
--- a/source/lib-intro.tex
+++ b/source/lib-intro.tex
@@ -390,12 +390,9 @@
 \item
 When invoking the function in a hardened implementation,
 prior to any other observable side effects of the function,
-one or more contract assertions
+contract assertions
 whose predicates are as described in the hardened precondition
-are evaluated with a checking semantic\iref{basic.contract.eval}.
-If any of these assertions is evaluated with a non-terminating semantic
-and the contract-violation handler returns,
-the program has undefined behavior.
+are evaluated with a terminating semantic\iref{basic.contract.eval}.
 \item
 When invoking the function in a non-hardened implementation,
 if any hardened precondition is violated,