diff --git a/doc/value/examples/parametrizing/context-depth.1.log b/doc/value/examples/parametrizing/context-depth.1.log
index 3f4497589cbc27fa521ad5ceb14ae2f1b9a7ea87..add271dee9176cff36bc65c00afff99ec9293cb6 100644
--- a/doc/value/examples/parametrizing/context-depth.1.log
+++ b/doc/value/examples/parametrizing/context-depth.1.log
@@ -77,3 +77,14 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/context-depth.2.log b/doc/value/examples/parametrizing/context-depth.2.log
index aa40ac4e166ab6994dcc729eda29c971fbc26b9c..872bda66319fccd4ef428f54fa1cfb2b7b4769a0 100644
--- a/doc/value/examples/parametrizing/context-depth.2.log
+++ b/doc/value/examples/parametrizing/context-depth.2.log
@@ -18,3 +18,14 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/context-depth.3.log b/doc/value/examples/parametrizing/context-depth.3.log
index 796a0b6e08f3e0952ff512a2f7bad3f25e026eda..b907017b2956d3f0ce7778a3ea9d5f7ed02c5529 100644
--- a/doc/value/examples/parametrizing/context-depth.3.log
+++ b/doc/value/examples/parametrizing/context-depth.3.log
@@ -13,3 +13,14 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/context-width.log b/doc/value/examples/parametrizing/context-width.log
index 9edcb21f15572a56426ca9304f0d6863bad55b3e..c586ab0c3b57b65077801e1f27d8eb031532480b 100644
--- a/doc/value/examples/parametrizing/context-width.log
+++ b/doc/value/examples/parametrizing/context-width.log
@@ -18,3 +18,14 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 2 statements reached (out of 2): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/global-initial-values.log b/doc/value/examples/parametrizing/global-initial-values.log
index f8a0ada3b0ebfb0280ec51512ac60ffbef5d0556..105b797c406f2d4a8edf73d82bd3963c5b8b8aa2 100644
--- a/doc/value/examples/parametrizing/global-initial-values.log
+++ b/doc/value/examples/parametrizing/global-initial-values.log
@@ -11,3 +11,14 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/ilevel.1.log b/doc/value/examples/parametrizing/ilevel.1.log
index c24bbec5ea55aafd4dd4ec002f046c27471d5397..de93eb9610ea6147566d6e9338bebe74f34ef9e4 100644
--- a/doc/value/examples/parametrizing/ilevel.1.log
+++ b/doc/value/examples/parametrizing/ilevel.1.log
@@ -21,3 +21,17 @@
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   __retres ∈ [2..31]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 5 statements reached (out of 5): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     1 valid     0 unknown     0 invalid      1 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/ilevel.2.log b/doc/value/examples/parametrizing/ilevel.2.log
index 49de84286e0f1c25406f1f449e8623c106750a82..8cef794e55af22fb5509812b86a3028f29cc12c6 100644
--- a/doc/value/examples/parametrizing/ilevel.2.log
+++ b/doc/value/examples/parametrizing/ilevel.2.log
@@ -21,3 +21,17 @@
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   __retres ∈ {2; 3; 5; 7; 11; 13; 17; 19; 23; 27; 29; 31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 5 statements reached (out of 5): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     1 valid     0 unknown     0 invalid      1 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/nor.1.log b/doc/value/examples/parametrizing/nor.1.log
index d9202d664a9fe97e59eaea38a4e1256f1bb8fbd9..292dfde5dd433ad2514ddf17d6ff9051303a918c 100644
--- a/doc/value/examples/parametrizing/nor.1.log
+++ b/doc/value/examples/parametrizing/nor.1.log
@@ -5,26 +5,26 @@
 [eva:initial-state] Values of globals at initialization
   t[0..1999] ∈ {0}
   i ∈ {0}
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
-[eva] Semantic level unrolling superposing up to 900 states
-[eva] Semantic level unrolling superposing up to 1000 states
-[eva] Semantic level unrolling superposing up to 1100 states
-[eva] Semantic level unrolling superposing up to 1200 states
-[eva] Semantic level unrolling superposing up to 1300 states
-[eva] Semantic level unrolling superposing up to 1400 states
-[eva] Semantic level unrolling superposing up to 1500 states
-[eva] Semantic level unrolling superposing up to 1600 states
-[eva] Semantic level unrolling superposing up to 1700 states
-[eva] Semantic level unrolling superposing up to 1800 states
-[eva] Semantic level unrolling superposing up to 1900 states
-[eva] Semantic level unrolling superposing up to 2000 states
+[eva] nor.c:5: Trace partitioning superposing up to 100 states
+[eva] nor.c:5: Trace partitioning superposing up to 200 states
+[eva] nor.c:5: Trace partitioning superposing up to 300 states
+[eva] nor.c:5: Trace partitioning superposing up to 400 states
+[eva] nor.c:5: Trace partitioning superposing up to 500 states
+[eva] nor.c:5: Trace partitioning superposing up to 600 states
+[eva] nor.c:5: Trace partitioning superposing up to 700 states
+[eva] nor.c:5: Trace partitioning superposing up to 800 states
+[eva] nor.c:5: Trace partitioning superposing up to 900 states
+[eva] nor.c:5: Trace partitioning superposing up to 1000 states
+[eva] nor.c:5: Trace partitioning superposing up to 1100 states
+[eva] nor.c:5: Trace partitioning superposing up to 1200 states
+[eva] nor.c:5: Trace partitioning superposing up to 1300 states
+[eva] nor.c:5: Trace partitioning superposing up to 1400 states
+[eva] nor.c:5: Trace partitioning superposing up to 1500 states
+[eva] nor.c:5: Trace partitioning superposing up to 1600 states
+[eva] nor.c:5: Trace partitioning superposing up to 1700 states
+[eva] nor.c:5: Trace partitioning superposing up to 1800 states
+[eva] nor.c:5: Trace partitioning superposing up to 1900 states
+[eva] nor.c:5: Trace partitioning superposing up to 2000 states
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function irrelevant_function:
@@ -4032,5 +4032,16 @@
    [1999] ∈ {1999}
   i ∈ {2000}
   __retres ∈ {143}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 10 statements reached (out of 10): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 
-user time: 0.61s
+user time: 7.67s
diff --git a/doc/value/examples/parametrizing/nor.2.log b/doc/value/examples/parametrizing/nor.2.log
index d79d6ad6a29371e5d6322a3cb2cb57eade5733ba..de472ed593d9225272ff7c5ed569b91e6601cd43 100644
--- a/doc/value/examples/parametrizing/nor.2.log
+++ b/doc/value/examples/parametrizing/nor.2.log
@@ -5,26 +5,26 @@
 [eva:initial-state] Values of globals at initialization
   t[0..1999] ∈ {0}
   i ∈ {0}
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
-[eva] Semantic level unrolling superposing up to 900 states
-[eva] Semantic level unrolling superposing up to 1000 states
-[eva] Semantic level unrolling superposing up to 1100 states
-[eva] Semantic level unrolling superposing up to 1200 states
-[eva] Semantic level unrolling superposing up to 1300 states
-[eva] Semantic level unrolling superposing up to 1400 states
-[eva] Semantic level unrolling superposing up to 1500 states
-[eva] Semantic level unrolling superposing up to 1600 states
-[eva] Semantic level unrolling superposing up to 1700 states
-[eva] Semantic level unrolling superposing up to 1800 states
-[eva] Semantic level unrolling superposing up to 1900 states
-[eva] Semantic level unrolling superposing up to 2000 states
+[eva] nor.c:5: Trace partitioning superposing up to 100 states
+[eva] nor.c:5: Trace partitioning superposing up to 200 states
+[eva] nor.c:5: Trace partitioning superposing up to 300 states
+[eva] nor.c:5: Trace partitioning superposing up to 400 states
+[eva] nor.c:5: Trace partitioning superposing up to 500 states
+[eva] nor.c:5: Trace partitioning superposing up to 600 states
+[eva] nor.c:5: Trace partitioning superposing up to 700 states
+[eva] nor.c:5: Trace partitioning superposing up to 800 states
+[eva] nor.c:5: Trace partitioning superposing up to 900 states
+[eva] nor.c:5: Trace partitioning superposing up to 1000 states
+[eva] nor.c:5: Trace partitioning superposing up to 1100 states
+[eva] nor.c:5: Trace partitioning superposing up to 1200 states
+[eva] nor.c:5: Trace partitioning superposing up to 1300 states
+[eva] nor.c:5: Trace partitioning superposing up to 1400 states
+[eva] nor.c:5: Trace partitioning superposing up to 1500 states
+[eva] nor.c:5: Trace partitioning superposing up to 1600 states
+[eva] nor.c:5: Trace partitioning superposing up to 1700 states
+[eva] nor.c:5: Trace partitioning superposing up to 1800 states
+[eva] nor.c:5: Trace partitioning superposing up to 1900 states
+[eva] nor.c:5: Trace partitioning superposing up to 2000 states
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -2031,5 +2031,16 @@ Cannot filter: dumping raw memory (including unchanged variables)
    [1999] ∈ {1999}
   i ∈ {2000}
   __retres ∈ {143}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 10 statements reached (out of 10): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 
-user time: 0.26s
+user time: 3.11s
diff --git a/doc/value/examples/parametrizing/out-of-bound.log b/doc/value/examples/parametrizing/out-of-bound.log
index 06f21f7998e676d93d8c108dbcd2b48ef71f4447..365e3edd937c7a33c60cbe1bb5381abda8849cb9 100644
--- a/doc/value/examples/parametrizing/out-of-bound.log
+++ b/doc/value/examples/parametrizing/out-of-bound.log
@@ -11,3 +11,16 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 2): 50% coverage.
+  In this function, 1 statements reached (out of 2): 50% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 access out of bounds index
+  1 of them is a sure alarm (invalid status).
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/simple-main.log b/doc/value/examples/parametrizing/simple-main.log
index d7defe1645a43850de824800f0e19a9bb6aff94f..63b112ec39394c71a88c5f29323ccf83fe27c333 100644
--- a/doc/value/examples/parametrizing/simple-main.log
+++ b/doc/value/examples/parametrizing/simple-main.log
@@ -19,3 +19,14 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 3 statements reached (out of 3): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/slevel.1.log b/doc/value/examples/parametrizing/slevel.1.log
index ca308071d5497e913e04fc07d678bf47f1c09be3..7fab16b9dd70afcef09736b1028774c06db758fd 100644
--- a/doc/value/examples/parametrizing/slevel.1.log
+++ b/doc/value/examples/parametrizing/slevel.1.log
@@ -12,3 +12,14 @@
   i ∈ {5}
   j ∈ {10}
   t[0..4][0..9] ∈ {1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/slevel.2.log b/doc/value/examples/parametrizing/slevel.2.log
index 9459da3c9930632a9ddf3d8c636f893133700702..cc1474f37db4dac630cbd75f34b91f3d24380ef9 100644
--- a/doc/value/examples/parametrizing/slevel.2.log
+++ b/doc/value/examples/parametrizing/slevel.2.log
@@ -14,3 +14,14 @@
   j ∈ {10}
   t{[0..1][0..9]; [2][0..5]} ∈ {1}
    {[2][6..9]; [3..4][0..9]} ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/widen-hints.log b/doc/value/examples/parametrizing/widen-hints.log
index 9e760a40d3385119f17618e60c584b5e1c63d888..b02525597d9e147f58fc3de93f49ce02e709d7d3 100644
--- a/doc/value/examples/parametrizing/widen-hints.log
+++ b/doc/value/examples/parametrizing/widen-hints.log
@@ -12,3 +12,14 @@
   i ∈ {13}
   j ∈ [0..55]
   n ∈ {13}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 9 statements reached (out of 9): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------