From ba34467f30eb49a0303297ac5eee09b084cabb14 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Mon, 25 Mar 2024 11:15:45 +0100
Subject: [PATCH] [doc] Add a hint to make the output more verbose in the ACAS
 tutorial

---
 doc/acas_xu.rst | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 7abf228..44d7071 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
-- 
GitLab