diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 7abf228bfc4fa257f3213cb18bdfb738543ff328..44d70717047cc494d319e9b3f1b421fedf1448ed 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -290,7 +290,9 @@ verifying the ACAS-Xu property :math:`\phi_1`:
     [caisar] Goal P1_1_1: Valid
 
 Note that the previous commands set the verification time limit to 10 minutes
-(*cf.* ``-t`` option).
+(*cf.* ``-t`` option). If you obtain a ``HighFailure`` error, you can
+troubleshoot it by increasing the verbosity of CAISAR's output (*cf.* ``-v``
+option).
 
 Under the hood, CAISAR first translates each goal into a compatible form for the
 targeted provers, then calls the provers on them, and finally interprets and