diff --git a/doc/eva/examples/parametrizing/context-depth.1.log b/doc/eva/examples/parametrizing/context-depth.1.log
index 139c36be08c48906b65b86276e6e3203918b3ecd..756c1a74b9b04adf88c42d4c3f09e26b9271a49d 100644
--- a/doc/eva/examples/parametrizing/context-depth.1.log
+++ b/doc/eva/examples/parametrizing/context-depth.1.log
@@ -1,7 +1,5 @@
 [kernel] Parsing context-depth.c (with preprocessing)
 [eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   s.v ∈ [--..--]
    .next ∈ {{ NULL ; &S_next_s[0] }}
@@ -73,7 +71,6 @@
   WELL_next_1_S_next_1_S_next_1_S_next_s[bits 0 to ..] ∈
                                         {{ garbled mix of &{WELL_next_1_S_next_1_S_next_1_S_next_s}
                                          (origin: Well) }}
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
diff --git a/doc/eva/examples/parametrizing/context-depth.2.log b/doc/eva/examples/parametrizing/context-depth.2.log
index ff79bd435cf102778218c423656dd13a60f37f5a..6b6aa0039525ac4abb58c47e36de65a38ca490f6 100644
--- a/doc/eva/examples/parametrizing/context-depth.2.log
+++ b/doc/eva/examples/parametrizing/context-depth.2.log
@@ -1,7 +1,5 @@
 [kernel] Parsing context-depth.c (with preprocessing)
 [eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   s.v ∈ [--..--]
    .next ∈ {{ NULL ; &S_next_s[0] }}
@@ -14,7 +12,6 @@
   WELL_next_0_S_next_0_S_next_s[bits 0 to ..] ∈
                                {{ garbled mix of &{WELL_next_0_S_next_0_S_next_s}
                                 (origin: Well) }}
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
diff --git a/doc/eva/examples/parametrizing/context-depth.3.log b/doc/eva/examples/parametrizing/context-depth.3.log
index 74df2d67c4c831fcce54fe160e0c3edb3c597ba8..c8db41f5ae99ea916b6f40838f1adff5f82f88fe 100644
--- a/doc/eva/examples/parametrizing/context-depth.3.log
+++ b/doc/eva/examples/parametrizing/context-depth.3.log
@@ -1,7 +1,5 @@
 [kernel] Parsing context-depth.c (with preprocessing)
 [eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   s.v ∈ [--..--]
    .next ∈ {{ &S_next_s[0] }}
@@ -9,7 +7,6 @@
           [0].next ∈ {{ &S_next_0_S_next_s[0] }}
   S_next_0_S_next_s[0].v ∈ [--..--]
                    [0].next ∈ {0}
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
diff --git a/doc/eva/examples/parametrizing/context-width.log b/doc/eva/examples/parametrizing/context-width.log
index c367004b639345fa6987b76d719d499e12387139..45b36f461fd793e4f3289cdd9d993aecc0622d25 100644
--- a/doc/eva/examples/parametrizing/context-width.log
+++ b/doc/eva/examples/parametrizing/context-width.log
@@ -1,7 +1,5 @@
 [kernel] Parsing context-width.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva] context-width.c:3: 
@@ -14,7 +12,6 @@
   S_0_S_t[0..1] ∈ [--..--]
   S_1_S_t[0..1] ∈ [--..--]
   ==END OF DUMP==
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
diff --git a/doc/eva/examples/parametrizing/global-initial-values.log b/doc/eva/examples/parametrizing/global-initial-values.log
index d92b41e0e4de3f190a5a81c5de117daca8faba96..d927c4ce3d0f950958c46462b9494063e616c623 100644
--- a/doc/eva/examples/parametrizing/global-initial-values.log
+++ b/doc/eva/examples/parametrizing/global-initial-values.log
@@ -1,13 +1,10 @@
 [kernel] Parsing global-initial-values.c (with preprocessing)
 [eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   s.i ∈ [--..--]
    .f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
    .p ∈ {{ NULL ; &S_p_s[0] }}
   S_p_s[0..1] ∈ [--..--]
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
diff --git a/doc/eva/examples/parametrizing/ilevel.1.log b/doc/eva/examples/parametrizing/ilevel.1.log
index 4c3c36a540cbfbfe0fc87fca46538cabc1d043ec..e8af55751ecf7b423ecd29a367bcf884d6737ecb 100644
--- a/doc/eva/examples/parametrizing/ilevel.1.log
+++ b/doc/eva/examples/parametrizing/ilevel.1.log
@@ -1,7 +1,5 @@
 [kernel] Parsing ilevel.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   t[0] ∈ {2}
    [1] ∈ {3}
@@ -16,7 +14,6 @@
    [10] ∈ {29}
    [11] ∈ {31}
 [eva] using specification for function Frama_C_interval
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
diff --git a/doc/eva/examples/parametrizing/ilevel.2.log b/doc/eva/examples/parametrizing/ilevel.2.log
index f1a8299dd21acb3880c10d023375f3664fcf89cf..879c0eacbfd241f33d916bafed2485dd6c793996 100644
--- a/doc/eva/examples/parametrizing/ilevel.2.log
+++ b/doc/eva/examples/parametrizing/ilevel.2.log
@@ -1,7 +1,5 @@
 [kernel] Parsing ilevel.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   t[0] ∈ {2}
    [1] ∈ {3}
@@ -16,7 +14,6 @@
    [10] ∈ {29}
    [11] ∈ {31}
 [eva] using specification for function Frama_C_interval
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
diff --git a/doc/eva/examples/parametrizing/loop-unroll-const.log b/doc/eva/examples/parametrizing/loop-unroll-const.log
index abece1184d370fff2faaad4d587fb08f25efcd15..bf574c8c35bce13349fdb0aff06c2df442fe0c16 100644
--- a/doc/eva/examples/parametrizing/loop-unroll-const.log
+++ b/doc/eva/examples/parametrizing/loop-unroll-const.log
@@ -1,12 +1,9 @@
 [kernel] Parsing loop-unroll-const.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva] loop-unroll-const.c:8: Trace partitioning superposing up to 100 states
 [eva] loop-unroll-const.c:8: Trace partitioning superposing up to 200 states
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   a[0][0] ∈ {0}
diff --git a/doc/eva/examples/parametrizing/loop-unroll-insuf.log b/doc/eva/examples/parametrizing/loop-unroll-insuf.log
index c32ca269286ffea19481c9361ae1a92de4779b58..2f6c5615a30203603203067e08a34053f013ca00 100644
--- a/doc/eva/examples/parametrizing/loop-unroll-insuf.log
+++ b/doc/eva/examples/parametrizing/loop-unroll-insuf.log
@@ -1,12 +1,9 @@
 [kernel] Parsing loop-unroll-insuf.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva:loop-unroll:partial] loop-unroll-insuf.c:4: loop not completely unrolled
 [eva] loop-unroll-insuf.c:4: starting to merge loop iterations
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   i ∈ {21}
diff --git a/doc/eva/examples/parametrizing/loop-unroll-nested.log b/doc/eva/examples/parametrizing/loop-unroll-nested.log
index b9f6861b432ed7b92c137e8cc0edacb3fe17bbfa..ae231bb674fc4165c165e4da0f7fc70257d78d61 100644
--- a/doc/eva/examples/parametrizing/loop-unroll-nested.log
+++ b/doc/eva/examples/parametrizing/loop-unroll-nested.log
@@ -1,7 +1,5 @@
 [kernel] Parsing loop-unroll-nested.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   t1[0] ∈ {1}
     [1] ∈ {2}
@@ -18,7 +16,6 @@
   sizes[0] ∈ {3}
        [1] ∈ {2}
        [2] ∈ {4}
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   S ∈ {45}
diff --git a/doc/eva/examples/parametrizing/out-of-bound.log b/doc/eva/examples/parametrizing/out-of-bound.log
index b61fb2c059ddc15ab2ac10f62281da02953ed5e5..08e2fc95baf70c6c6c9e6da061909c1f2ad8a524 100644
--- a/doc/eva/examples/parametrizing/out-of-bound.log
+++ b/doc/eva/examples/parametrizing/out-of-bound.log
@@ -1,12 +1,9 @@
 [kernel] Parsing out-of-bound.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   t[0..9][0..9] ∈ {0}
 [eva:alarm] out-of-bound.c:4: Warning: 
   accessing out of bounds index. assert 12 < 10;
-[eva] Done for function main
 [eva] out-of-bound.c:4: assertion 'Eva,index_bound' got final status invalid.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
diff --git a/doc/eva/examples/parametrizing/recursion-imprecise.log b/doc/eva/examples/parametrizing/recursion-imprecise.log
index e9ab172dd1b55a46da2c7345440a0c26f3c281d0..48fbae74ac0c729172c2f2a8d675e47ccc59537b 100644
--- a/doc/eva/examples/parametrizing/recursion-imprecise.log
+++ b/doc/eva/examples/parametrizing/recursion-imprecise.log
@@ -1,7 +1,5 @@
 [kernel] Parsing recursion-imprecise.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva] recursion-imprecise.c:3: Frama_C_show_each: [-2147483648..2147483647]
@@ -20,7 +18,6 @@
 [eva:alarm] recursion-imprecise.c:5: Warning: 
   signed overflow. assert 1 + tmp ≤ 2147483647;
                    (tmp from mod3(x - 1))
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function mod3:
   __retres ∈ [-2147483647..2147483647]
diff --git a/doc/eva/examples/parametrizing/recursion-simple.log b/doc/eva/examples/parametrizing/recursion-simple.log
index 632ec4e578cd475b3b1b85033474f7b4242a9fe3..0a70eae0e40e6573684336563308b2e90d9f747f 100644
--- a/doc/eva/examples/parametrizing/recursion-simple.log
+++ b/doc/eva/examples/parametrizing/recursion-simple.log
@@ -1,7 +1,5 @@
 [kernel] Parsing recursion-simple.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva:recursion] recursion-simple.c:4: 
@@ -17,7 +15,6 @@
 [eva:alarm] recursion-simple.c:4: Warning: 
   signed overflow. assert i * tmp ≤ 2147483647;
                    (tmp from factorial(i - 1))
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function factorial:
   __retres ∈ [-2147483646..2147483646]
diff --git a/doc/eva/examples/parametrizing/simple-main.log b/doc/eva/examples/parametrizing/simple-main.log
index e311d13d995638fc568b4e01b3b803e136041cd2..644c0d9fff33d0796477a2c6ecaf5aefb044c17c 100644
--- a/doc/eva/examples/parametrizing/simple-main.log
+++ b/doc/eva/examples/parametrizing/simple-main.log
@@ -1,7 +1,5 @@
 [kernel] Parsing simple-main.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva] simple-main.c:3: 
@@ -15,7 +13,6 @@
   S_0_S_argv[0..1] ∈ [--..--]
   S_1_S_argv[0..1] ∈ [--..--]
   ==END OF DUMP==
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   __retres ∈ {0}
diff --git a/doc/eva/examples/parametrizing/slevel.1.log b/doc/eva/examples/parametrizing/slevel.1.log
index cb90f0bf0a5b63bde1d1b72575d3abc1f9d441d3..23ba8a394437903f669ea532d3a71e1ffb3e1414 100644
--- a/doc/eva/examples/parametrizing/slevel.1.log
+++ b/doc/eva/examples/parametrizing/slevel.1.log
@@ -1,12 +1,9 @@
 [kernel] Parsing slevel.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   i ∈ {0}
   j ∈ {0}
   t[0..4][0..9] ∈ {0}
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   i ∈ {5}
diff --git a/doc/eva/examples/parametrizing/slevel.2.log b/doc/eva/examples/parametrizing/slevel.2.log
index 7c279db06037e0ab36b95ea474b439bf3650e148..507d3eaf172617e34eb4ebb489e8efa51dc4861d 100644
--- a/doc/eva/examples/parametrizing/slevel.2.log
+++ b/doc/eva/examples/parametrizing/slevel.2.log
@@ -1,13 +1,10 @@
 [kernel] Parsing slevel.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   i ∈ {0}
   j ∈ {0}
   t[0..4][0..9] ∈ {0}
 [eva] slevel.c:6: starting to merge loop iterations
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   i ∈ {5}
diff --git a/doc/eva/examples/parametrizing/split-array.log b/doc/eva/examples/parametrizing/split-array.log
index ab9cf49866f9cde4c7964cb556875e2f7b5d2443..b481c748a10c1d99cb0ba9d587c71e50806f51c7 100644
--- a/doc/eva/examples/parametrizing/split-array.log
+++ b/doc/eva/examples/parametrizing/split-array.log
@@ -1,7 +1,5 @@
 [kernel] Parsing split-array.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   t1[0] ∈ {1}
     [1] ∈ {2}
@@ -20,7 +18,6 @@
        [2] ∈ {4}
 [eva:alarm] split-array.c:4: Warning: 
   function main: precondition got status unknown.
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   S ∈ {6; 9; 30}
diff --git a/doc/eva/examples/parametrizing/split-fabs.log b/doc/eva/examples/parametrizing/split-fabs.log
index 018de826611f6a87e0f8549714fe633a71a71744..c9bb061d6e1705fac56f84d1dc40b9a9a4c3d61a 100644
--- a/doc/eva/examples/parametrizing/split-fabs.log
+++ b/doc/eva/examples/parametrizing/split-fabs.log
@@ -1,10 +1,7 @@
 [kernel] Parsing split-fabs.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function fabs:
   
diff --git a/doc/eva/examples/parametrizing/widen-hints.log b/doc/eva/examples/parametrizing/widen-hints.log
index de623374476a5a628f2d98e80efcf3201e56ccc0..9caa65eaf79d7a1f352ce455dae5bc7932405870 100644
--- a/doc/eva/examples/parametrizing/widen-hints.log
+++ b/doc/eva/examples/parametrizing/widen-hints.log
@@ -1,12 +1,9 @@
 [kernel] Parsing widen-hints.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   i ∈ {0}
   j ∈ {0}
 [eva] widen-hints.c:6: starting to merge loop iterations
-[eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   i ∈ {13}
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index c6828328a6b78713b496eb2ea58985723f08e7c4..7e8914b886b054af19ff211b78fe16db6ca1bc2a 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -3091,7 +3091,7 @@ prototype of \lstinline|main| is:
 \cwithrange{1-1}{examples/parametrizing/simple-main.c}
 The types of arguments \lstinline|argc| and \lstinline|argv|
 translate into the following initial values:
-\logwithrange{10-16}{examples/parametrizing/simple-main.log}
+\logwithrange{8-14}{examples/parametrizing/simple-main.log}
 
 This is generally not what is wanted, but then again, embedded applications
 are generally not written against the POSIX interface. If the analyzed
@@ -3198,7 +3198,7 @@ also decided by the value of option \lstinline|-eva-context-width|.
 Example: with the default value \lstinline|2| for option
 \lstinline|-eva-context-width|, the declaration \lstinline|int *(t[5]);|
 causes the following array to be allocated:
-\logwithrange{10-15}{examples/parametrizing/context-width.log}
+\logwithrange{8-13}{examples/parametrizing/context-width.log}
 
 Note that for both arrays of pointers and pointers to pointers,
 using option \lstinline|-eva-context-width 1| corresponds to a very strong
@@ -3223,7 +3223,7 @@ two is plenty for most programs.
 For instance, here is part of the initial state displayed by \Eva{}
 in \lstinline|-lib-entry| mode if a global variable \lstinline|s|
 has the type \lstinline|struct S| defined above:
-\logwithrange{6-17}{examples/parametrizing/context-depth.1.log}
+\logwithrange{4-15}{examples/parametrizing/context-depth.1.log}
 
 In this case, if variable \lstinline|s| is the only one which
 is automatically allocated, it makes sense to set the option
@@ -3237,7 +3237,7 @@ Below are the initial contents for a variable \lstinline|s| of type \lstinline|s
 with options \lstinline|-eva-context-width 1|
 \lstinline|-eva-context-depth 1|:
 
-\logwithrange{6-16}{examples/parametrizing/context-depth.2.log}
+\logwithrange{4-14}{examples/parametrizing/context-depth.2.log}
 
 \subsubsection{The possibility of invalid pointers}
 
@@ -3271,7 +3271,7 @@ a variable \lstinline|s| of
 type \lstinline|struct S| receives  the following initial contents,
 modeling a chained list of length exactly 3:
 
-\logwithrange{6-11}{examples/parametrizing/context-depth.3.log}
+\logwithrange{4-9}{examples/parametrizing/context-depth.3.log}
 
 \subsection{State of the IEEE 754 environment}
 
@@ -3395,7 +3395,7 @@ alarm. This leads to an alarm on the following example:
 \Eva{} assumes that writing \lstinline|t[0][...]|, the programmer
 intended the memory access to be inside \lstinline|t[0]|. Consequently,
 it emits an alarm:
-\logwithrange{8-8}{examples/parametrizing/out-of-bound.log}
+\logwithrange{5-6}{examples/parametrizing/out-of-bound.log}
 The option \lstinline|-unsafe-arrays| tells \Eva{} to warn
 only if the address as computed using its modeling of pointer arithmetics
 is invalid. With the option, \Eva{} does not warn about line 4
@@ -3503,7 +3503,7 @@ in the general case and will instead rely on the \lstinline|mod3| specification,
 as it cannot reduce the new argument value of the recursive calls, as shown
 by the successive values printed by the \lstinline|Frama_C_show_each| directive:
 
-\logwithrange{12-19}{examples/parametrizing/recursion-imprecise.log}
+\logwithrange{10-17}{examples/parametrizing/recursion-imprecise.log}
 
 Finally, note that the unrolling of a very large number of recursive calls can
 considerably slow down the analysis.
@@ -3672,10 +3672,10 @@ the specified unrolling value is insufficient to unroll the loop entirely:
 
 \csource{examples/parametrizing/loop-unroll-insuf.c}
 
-\logwithrange{7-7}
+\logwithrange{5-5}
   {examples/parametrizing/loop-unroll-insuf.log}
 
-The message can be deactived via \lstinline|-eva-warn-key loop-unroll=inactive|.
+The message can be disabled via \lstinline|-eva-warn-key loop-unroll=inactive|.
 
 Note that using an unrolling parameter which is higher than the actual number
 of iterations of a loop doesn't generally have an effect on the analysis.
@@ -3711,7 +3711,7 @@ option \lstinline|-eva-slevel 55| in order to be completely unrolled:
 
 When the loops are sufficiently unrolled, the result obtained for the
 contents of array \lstinline|t| are the optimally precise:
-\logwithrange{14-14}{examples/parametrizing/slevel.1.log}
+\logwithrange{11-11}{examples/parametrizing/slevel.1.log}
 
 The number to pass the option \lstinline|-eva-slevel|  is of the magnitude of
 the number of values for \lstinline|i| (the 6 integers between 0 and 5)
@@ -3720,7 +3720,7 @@ integers comprised between 0 and 10). If a value much lower than
 this is passed, the result of the initialization of array \lstinline|t|
 will only be precise for the first cells. The option \lstinline|-eva-slevel 28|
 gives for instance the following result for array \lstinline|t|:
-\logwithrange{15-16}{examples/parametrizing/slevel.2.log}
+\logwithrange{12-13}{examples/parametrizing/slevel.2.log}
 
 In this result, the effects of the first iterations of the loops
 (for the whole of \lstinline|t[0]|, the whole of \lstinline|t[1]| and the first
@@ -3994,7 +3994,7 @@ evaluated by \Eva{} as a singleton in each case, which enables the use of a
 the function can be exactly computed as the set of three possible values instead
 of an imprecise interval.
 
-\logwithrange{25-26}{examples/parametrizing/split-array.log}
+\logwithrange{22-23}{examples/parametrizing/split-array.log}
 
 A \lstinline|split| annotation can be used on any expression that evaluates to a
 {\it small} number of integer values. In particular, the expression can be a C
@@ -4129,13 +4129,13 @@ Example:
 With the default limit of 8 elements for sets of integers, the
 analysis of the program shows a correct but approximated result:
 
-\logwithrange{23-23}{examples/parametrizing/ilevel.1.log}
+\logwithrange{20-20}{examples/parametrizing/ilevel.1.log}
 
 Studying the program, the user may decide to improve the precision of
 the result by adding \verb|-eva-ilevel 16| to the command line. The
 analysis result then becomes:
 
-\logwithrange{23-23}{examples/parametrizing/ilevel.2.log}
+\logwithrange{20-20}{examples/parametrizing/ilevel.2.log}
 
 \subsection{Maximum number of precise items in arrays}