diff --git a/cerberus/.frama-c/cheri_07_wide.eva/warnings.log b/cerberus/.frama-c/cheri_07_wide.eva/warnings.log
index 76958fa83df051b3dcfdf4e99f6be3041b8c0355..3cdf16b5d94390388930fbb168f4233f8a388b70 100644
--- a/cerberus/.frama-c/cheri_07_wide.eva/warnings.log
+++ b/cerberus/.frama-c/cheri_07_wide.eva/warnings.log
@@ -1,3 +1,2 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 cheri_07_wide.c:10:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 cheri_07_wide.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
diff --git a/cerberus/.frama-c/compcertTSO-1.eva/warnings.log b/cerberus/.frama-c/compcertTSO-1.eva/warnings.log
index 5880780ea1103b115ec7ac70bf68f02a8cda9e72..4a397709dd630278b0c13c2d5b1cebb57795893f 100644
--- a/cerberus/.frama-c/compcertTSO-1.eva/warnings.log
+++ b/cerberus/.frama-c/compcertTSO-1.eva/warnings.log
@@ -1,3 +1,2 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 compcertTSO-1.c:8:[eva:locals-escaping] warning: locals {a} escaping the scope of f through \result<f>
 compcertTSO-1.c:8:[eva:locals-escaping] warning: locals {a} escaping the scope of g through \result<g>
diff --git a/cerberus/.frama-c/null_pointer_4.eva/warnings.log b/cerberus/.frama-c/null_pointer_4.eva/warnings.log
index 14647f2485bd840524d36da174531e6de0237c15..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/cerberus/.frama-c/null_pointer_4.eva/warnings.log
+++ b/cerberus/.frama-c/null_pointer_4.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/padding_subunion_1.eva/warnings.log b/cerberus/.frama-c/padding_subunion_1.eva/warnings.log
index 6dd22532c71a7986c9d79f214e93808b3f2584a0..77839f1a9108487f674a9d242623eb32de248314 100644
--- a/cerberus/.frama-c/padding_subunion_1.eva/warnings.log
+++ b/cerberus/.frama-c/padding_subunion_1.eva/warnings.log
@@ -1,3 +1,2 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 padding_subunion_1.c:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
diff --git a/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log b/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log
index 14647f2485bd840524d36da174531e6de0237c15..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log
+++ b/cerberus/.frama-c/padding_unspecified_value_5.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log b/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log
index 14647f2485bd840524d36da174531e6de0237c15..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log
+++ b/cerberus/.frama-c/pointer_arith_algebraic_properties_2_global.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log b/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log
index dd8bf5f199da158402c7d2d47e09dfa79688753e..5f466f9859c64c4e452025c954f69296a791c3f5 100644
--- a/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log
+++ b/cerberus/.frama-c/pointer_offset_xor_auto.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 [eva:garbled-mix] warning: Garbled mix generated during analysis:
 {{ garbled mix of &{y} (origin: Arithmetic {pointer_offset_xor_auto.c:7}) }}
 {{ garbled mix of &{x} (origin: Arithmetic {pointer_offset_xor_auto.c:7}) }}
diff --git a/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log b/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log
index 0b296c6fb0e0e04e7bff346d38c9eee71efe6859..83184169fbaa485d5621bd1ba4963a46121d14b4 100644
--- a/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 provenance_basic_malloc_offset+12.c:4:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
 provenance_basic_malloc_offset+12.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
diff --git a/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log b/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log
index c4a4f6aeecd0457bf7ec442002e4179878247803..af084233f67f41e72e0c57c358e385a80109a070 100644
--- a/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_basic_using_intptr_t_auto_yx.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 provenance_basic_using_intptr_t_auto_yx.c:8:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_using_intptr_t_auto_yx.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
diff --git a/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log b/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log
index 14647f2485bd840524d36da174531e6de0237c15..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_equality_auto_cu_yx_b.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log b/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log
index 293d8de2d57dc93ca08d5f58a64385357d6935f8..1fcfffd06835e4ae359c066c72768b64c047eb52 100644
--- a/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log
+++ b/cerberus/.frama-c/provenance_via_io_bytewise_global.eva/warnings.log
@@ -1,4 +1,3 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
 provenance_via_io_bytewise_global.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 provenance_via_io_bytewise_global.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
 provenance_via_io_bytewise_global.c:14:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
diff --git a/cerberus/.frama-c/trap_representation_3.eva/warnings.log b/cerberus/.frama-c/trap_representation_3.eva/warnings.log
index 14647f2485bd840524d36da174531e6de0237c15..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/cerberus/.frama-c/trap_representation_3.eva/warnings.log
+++ b/cerberus/.frama-c/trap_representation_3.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log b/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log
index 14647f2485bd840524d36da174531e6de0237c15..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log
+++ b/cerberus/.frama-c/unspecified_value_representation_bytes_1.eva/warnings.log
@@ -1 +0,0 @@
-[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.