diff --git a/doc/mnist.rst b/doc/mnist.rst
index 6570d7dd2de1fa628346ea7a73a405f63d5ae5ba..38e0e98a10aaefb6c30d5630020a1c88b6bab3b3 100644
--- a/doc/mnist.rst
+++ b/doc/mnist.rst
@@ -92,7 +92,7 @@ to declare and define :math:`\epsilon`.
    type label_ = int
 
 We will first write some predicates to take into account the fact
-that we only have two available labels in the dataset sample (0, 1 and 2)
+that MNIST counts 10 labels (integer from 0 to 9) in the dataset sample,
 and that the
 input images are normalized (floating point values between 0. and 1.).
 We will also define a predicate that, given a label ``l`` and an image ``i``, checks whether the neural network ``nn`` indeed advises the correct label.
@@ -102,13 +102,13 @@ We will also define a predicate that, given a label ``l`` and an image ``i``, ch
    predicate valid_image (i: image) =
      forall v: index. valid_index i v -> (0.0: t) .<= i[v] .<= (1.0: t)
   
-   predicate valid_label (l: label_) = 0 <= l <= 2
+   predicate valid_label (l: label_) = 0 <= l <= 9
   
    predicate advises (n: nn) (i: image) (l: label_) =
      valid_label l ->
      forall j: int. valid_label j ->  j <> l -> (n@@i)[l] .> (n@@i)[j]
 
-We write that :math:`\lVert x - x' \rVert_\infty \leq \epsilon` with another
+We write :math:`\lVert x - x' \rVert_\infty \leq \epsilon` with another
 predicate:
 
 .. code-block:: whyml
@@ -139,8 +139,8 @@ samples, we can define a goal and check the property
 .. code-block:: whyml
 
   goal robustness:
-    let nn = read_neural_network "MNIST_256_2" ONNX in
-    let dataset = read_dataset "mnist_test.csv" CSV in
+    let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
+    let dataset = read_dataset "csv/mnist_test.csv" CSV in
     let eps = (0.375:t) in
     robust nn dataset eps
 
@@ -161,7 +161,7 @@ done via CAISAR as follows:
 
 .. code-block:: console
 
-   $ caisar verify --prover nnenum -L examples/mnist/nets --format whyml examples/mnist/property.why
+   $ caisar verify --prover nnenum -L examples/mnist/ --format whyml examples/mnist/property.why
    [caisar] Goal robustness: Invalid
 
 The result tells us that there exists at least one image in ``mnist_test.csv``
diff --git a/examples/mnist/property.why b/examples/mnist/property.why
index 24cfa42801b4645b83ad85c6ffa5ff16313199ef..3a98618b79e94a702661efbe6dfe1650d3d0c77b 100644
--- a/examples/mnist/property.why
+++ b/examples/mnist/property.why
@@ -11,7 +11,7 @@ theory MNIST
   predicate valid_image (i: image) =
     forall v: index. valid_index i v -> (0.0: t) .<= i[v] .<= (1.0: t)
 
-  predicate valid_label (l: label_) = 0 <= l <= 2
+  predicate valid_label (l: label_) = 0 <= l <= 9
 
   predicate advises (n: nn) (i: image) (l: label_) =
     valid_label l ->
@@ -32,8 +32,8 @@ theory MNIST
     Dataset.forall_ d (robust_around n eps)
 
   goal robustness:
-    let nn = read_neural_network "MNIST_256_2" ONNX in
-    let dataset = read_dataset "mnist_test.csv" CSV in
+    let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
+    let dataset = read_dataset "csv/mnist_test.csv" CSV in
     let eps = (0.375:t) in
     robust nn dataset eps
 end