diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 469ad4d12172f27c844f81777bcbbc854b84c545..2e4a586c5ebd16205bb72e6d0746d2ec65a19a76 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -247,19 +247,16 @@ verifying the ACAS-Xu property :math:`\phi_1`:
 
 .. code-block:: console
 
-    $ caisar verify --prover Marabou -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_1.why -t 10m
+    $ caisar verify --prover Marabou examples/acasxu/property_1.why -t 10m
     [caisar] Goal P1_1_1: Timeout
 
 .. code-block:: console
 
-    $ caisar verify --prover nnenum -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_1.why -t 10m
+    $ caisar verify --prover nnenum examples/acasxu/property_1.why -t 10m
     [caisar] Goal P1_1_1: Valid
 
 Note that the previous commands set the verification time limit to 10 minutes
-(*cf.* ``-t`` option), and the additional location ``examples/acasxu/nets/onnx``
-(*cf.* ``-L`` option) for letting CAISAR correctly locate the neural network
-file ``ACASXU_1_1.onnx`` that is used by the ``ACASXU_P1`` theory in
-``property_1.why``.
+(*cf.* ``-t`` 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
@@ -340,13 +337,13 @@ We can then verify the resulting verification problem as before:
 
 .. code-block:: console
 
-    $ caisar verify --prover Marabou -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_3.why -t 10m
+    $ caisar verify --prover Marabou examples/acasxu/property_3.why -t 10m
     [caisar] Goal P3_1_1: Timeout
     [caisar] Goal P3_2_7: Valid
 
 .. code-block:: console
 
-    $ caisar verify --prover nnenum -L examples/acasxu/nets/onnx --format whyml examples/acasxu/property_3.why -t 10m
+    $ caisar verify --prover nnenum examples/acasxu/property_3.why -t 10m
     [caisar] Goal P3_1_1: Valid
     [caisar] Goal P3_2_7: Valid