Skip to content
Snippets Groups Projects
Commit ba34467f authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

[doc] Add a hint to make the output more verbose in the ACAS tutorial

parent 45581f16
No related branches found
No related tags found
No related merge requests found
...@@ -290,7 +290,9 @@ verifying the ACAS-Xu property :math:`\phi_1`: ...@@ -290,7 +290,9 @@ verifying the ACAS-Xu property :math:`\phi_1`:
[caisar] Goal P1_1_1: Valid [caisar] Goal P1_1_1: Valid
Note that the previous commands set the verification time limit to 10 minutes 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 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 targeted provers, then calls the provers on them, and finally interprets and
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment