diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 0ad642e6662c886407ad0f4a0d9af27f99c2b043..305eb99a8ac94cc02c0e8cff90b1f82f73ed1e51 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -19,7 +19,7 @@ PROJECT_FILE.i:138:[value] Assertion got status unknown.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 17272a476aea2254c6fadcf0758919134032b9ab..d1c35002514a4f04b1feadb5087dc34273b7f029 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -7,11 +7,11 @@ tests/e-acsl-runtime/cast.i:18:[e-acsl] warning: missing guard for ensuring that
 PROJECT_FILE.i:134:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_str <- main.
         Called from PROJECT_FILE.i:136.
-PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown
+PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown.
 [value] Done for function mpz_init_set_str
 [value] computing for function mpz_get_si <- main.
         Called from PROJECT_FILE.i:137.
-PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid
+PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid.
 [value] Done for function mpz_get_si
 [value] computing for function e_acsl_fail <- main.
         Called from PROJECT_FILE.i:138.
@@ -20,13 +20,13 @@ PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:139.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 PROJECT_FILE.i:142:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_str <- main.
@@ -34,7 +34,7 @@ PROJECT_FILE.i:142:[value] Assertion got status valid.
 [value] Done for function mpz_init_set_str
 [value] computing for function mpz_get_ui <- main.
         Called from PROJECT_FILE.i:145.
-PROJECT_FILE.i:96:[value] Function mpz_get_ui: precondition got status valid
+PROJECT_FILE.i:96:[value] Function mpz_get_ui: precondition got status valid.
 [value] Done for function mpz_get_ui
 [value] computing for function e_acsl_fail <- main.
         Called from PROJECT_FILE.i:147.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index d5de2bfad5f39345bd2b648f99b96177f0259862..ba903d11580edd9956268f70a40b96e092b4401a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -7,15 +7,15 @@ PROJECT_FILE.i:138:[value] Assertion got status valid.
 PROJECT_FILE.i:141:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:143.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:143.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
         Called from PROJECT_FILE.i:144.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
         Called from PROJECT_FILE.i:145.
@@ -24,13 +24,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:146.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:146.
@@ -75,12 +75,12 @@ PROJECT_FILE.i:182:[value] Assertion got status valid.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
         Called from PROJECT_FILE.i:184.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
         Called from PROJECT_FILE.i:185.
-PROJECT_FILE.i:55:[value] Function mpz_neg: precondition got status valid
-PROJECT_FILE.i:56:[value] Function mpz_neg: precondition got status valid
+PROJECT_FILE.i:55:[value] Function mpz_neg: precondition got status valid.
+PROJECT_FILE.i:56:[value] Function mpz_neg: precondition got status valid.
 [value] Done for function mpz_neg
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:185.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index a1bf328b27036762ca862ba48182e47abf2869c7..81ba3e72ab9b4915c53af9910c13d288d78d5692 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -6,29 +6,29 @@
         Y ∈ {2}
 [value] computing for function f <- main.
         Called from PROJECT_FILE.i:346.
-PROJECT_FILE.i:129:[value] Function f: postcondition got status valid
+PROJECT_FILE.i:129:[value] Function f: postcondition got status valid.
 [value] Recording results for f
 [value] Done for function f
 [value] computing for function g <- main.
         Called from PROJECT_FILE.i:347.
-PROJECT_FILE.i:143:[value] Function g: postcondition got status valid
-PROJECT_FILE.i:144:[value] Function g: postcondition got status valid
+PROJECT_FILE.i:143:[value] Function g: postcondition got status valid.
+PROJECT_FILE.i:144:[value] Function g: postcondition got status valid.
 [value] Recording results for g
 [value] Done for function g
 [value] computing for function h <- main.
         Called from PROJECT_FILE.i:348.
-PROJECT_FILE.i:162:[value] Function h: precondition got status valid
+PROJECT_FILE.i:162:[value] Function h: precondition got status valid.
 [value] computing for function mpz_init_set_si <- h <- main.
         Called from PROJECT_FILE.i:166.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- h <- main.
         Called from PROJECT_FILE.i:166.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- h <- main.
         Called from PROJECT_FILE.i:167.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- h <- main.
         Called from PROJECT_FILE.i:168.
@@ -37,13 +37,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- h <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- h <- main.
         Called from PROJECT_FILE.i:169.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- h <- main.
         Called from PROJECT_FILE.i:169.
@@ -52,8 +52,8 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
 [value] Done for function h
 [value] computing for function i <- main.
         Called from PROJECT_FILE.i:349.
-PROJECT_FILE.i:176:[value] Function i: precondition got status valid
-PROJECT_FILE.i:177:[value] Function i: precondition got status valid
+PROJECT_FILE.i:176:[value] Function i: precondition got status valid.
+PROJECT_FILE.i:177:[value] Function i: precondition got status valid.
 [value] computing for function mpz_init_set_si <- i <- main.
         Called from PROJECT_FILE.i:181.
 [value] Done for function mpz_init_set_si
@@ -108,9 +108,9 @@ PROJECT_FILE.i:177:[value] Function i: precondition got status valid
 [value] Done for function i
 [value] computing for function j <- main.
         Called from PROJECT_FILE.i:350.
-PROJECT_FILE.i:196:[value] Function j, behavior b1: precondition got status valid
-PROJECT_FILE.i:200:[value] Function j, behavior b2: precondition got status valid
-PROJECT_FILE.i:201:[value] Function j, behavior b2: precondition got status valid
+PROJECT_FILE.i:196:[value] Function j, behavior b1: precondition got status valid.
+PROJECT_FILE.i:200:[value] Function j, behavior b2: precondition got status valid.
+PROJECT_FILE.i:201:[value] Function j, behavior b2: precondition got status valid.
 [value] computing for function mpz_init_set_si <- j <- main.
         Called from PROJECT_FILE.i:211.
 [value] Done for function mpz_init_set_si
@@ -141,13 +141,13 @@ PROJECT_FILE.i:201:[value] Function j, behavior b2: precondition got status vali
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- j <- main.
         Called from PROJECT_FILE.i:215.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown.
 [value] Done for function mpz_init
 [value] computing for function mpz_add <- j <- main.
         Called from PROJECT_FILE.i:216.
-PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
+PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid.
 [value] Done for function mpz_add
 [value] computing for function mpz_cmp <- j <- main.
         Called from PROJECT_FILE.i:217.
@@ -205,15 +205,15 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
 [value] computing for function mpz_clear <- j <- main.
         Called from PROJECT_FILE.i:224.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:197:[value] Function j, behavior b1: postcondition got status valid
-PROJECT_FILE.i:202:[value] Function j, behavior b2: postcondition got status valid
+PROJECT_FILE.i:197:[value] Function j, behavior b1: postcondition got status valid.
+PROJECT_FILE.i:202:[value] Function j, behavior b2: postcondition got status valid.
 [value] Recording results for j
 [value] Done for function j
 [value] computing for function k <- main.
         Called from PROJECT_FILE.i:351.
-PROJECT_FILE.i:247:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated
-PROJECT_FILE.i:252:[value] Function k, behavior b2: precondition got status valid
-PROJECT_FILE.i:253:[value] Function k, behavior b2: precondition got status valid
+PROJECT_FILE.i:247:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
+PROJECT_FILE.i:252:[value] Function k, behavior b2: precondition got status valid.
+PROJECT_FILE.i:253:[value] Function k, behavior b2: precondition got status valid.
 [value] computing for function mpz_init_set_si <- k <- main.
         Called from PROJECT_FILE.i:266.
 [value] Done for function mpz_init_set_si
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 88791a2fee6a73426f7b08d2c6c24c02ffe2472f..dd65f0697655184082c19b01fc680d3124de58e1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -7,15 +7,15 @@ PROJECT_FILE.i:135:[value] Assertion got status valid.
 PROJECT_FILE.i:138:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_str <- main.
         Called from PROJECT_FILE.i:140.
-PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown
+PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown.
 [value] Done for function mpz_init_set_str
 [value] computing for function mpz_init_set_str <- main.
         Called from PROJECT_FILE.i:141.
 [value] Done for function mpz_init_set_str
 [value] computing for function mpz_cmp <- main.
         Called from PROJECT_FILE.i:142.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
         Called from PROJECT_FILE.i:144.
@@ -24,13 +24,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:145.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:145.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index ab2a39e9d573e0f55ff468d85eeca5fbfa175264..f0693c50a44cfca3ee84058434500a1c2ed63a79 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -6,15 +6,15 @@ tests/e-acsl-runtime/nested_code_annot.i:12:[kernel] warning: Body of function m
 PROJECT_FILE.i:134:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:141.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:141.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
         Called from PROJECT_FILE.i:142.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
         Called from PROJECT_FILE.i:143.
@@ -23,13 +23,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:144.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:144.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index f4920b640721625ad727434e3fee7829d832fa14..f0c78ccd69af31f45afce818ac8d934b261df275 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -6,15 +6,15 @@ PROJECT_FILE.i:134:[value] Assertion got status valid.
 PROJECT_FILE.i:137:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:139.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:139.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
         Called from PROJECT_FILE.i:140.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
         Called from PROJECT_FILE.i:141.
@@ -23,13 +23,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:142.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:142.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 3664a2e1cb30844326dbdf51cf747ec13ff8735a..e0448b250d0a9f46ad7aceb731ad9df34efa8752 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -5,15 +5,15 @@
 PROJECT_FILE.i:131:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:133.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
         Called from PROJECT_FILE.i:133.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
         Called from PROJECT_FILE.i:134.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
         Called from PROJECT_FILE.i:135.
@@ -22,13 +22,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:136.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:136.