diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 2a64bdb4a4631a51b14794f6502d000893b8b3ec..d0ea7ffc08385be12d97dd9b01c69d8c2e0a5199 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -1,5 +1,7 @@
+- mkcall ne devrait pas générer de nouvelles variables pour une même fonction
+- mettre des locations intelligentes
+
 - intégration à la ferme de tests nocturne
-- cas d'utilisation et link avec gmp
 
 - guarde pour les divisions/modulos
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 462f26204da38d60cf995e0d89212a15124db7c5..037892419400db7546258b66a7e80bfc663aba73 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -5,23 +5,24 @@
 PROJECT_FILE.i:123:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:125:[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 <-main.
         Called from PROJECT_FILE.i:126.
-PROJECT_FILE.i:126:[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:126.
-PROJECT_FILE.i:126:[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:127.
-PROJECT_FILE.i:127:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:128.
-PROJECT_FILE.i:128:[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:129.
@@ -30,41 +31,35 @@ PROJECT_FILE.i:128:[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:115.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:105:[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:130.
-PROJECT_FILE.i:130:[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:130.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:131.
-PROJECT_FILE.i:131:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:134:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:136.
-PROJECT_FILE.i:136:[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:137.
-PROJECT_FILE.i:137:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:137.
-PROJECT_FILE.i:137:[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:138.
-PROJECT_FILE.i:138:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:139.
-PROJECT_FILE.i:139:[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:140.
@@ -78,27 +73,22 @@ PROJECT_FILE.i:139:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:141.
-PROJECT_FILE.i:141:[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:141.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:142.
-PROJECT_FILE.i:142:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:145:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:147.
-PROJECT_FILE.i:147:[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:148.
-PROJECT_FILE.i:148:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:148.
-PROJECT_FILE.i:148:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_com <-main.
         Called from PROJECT_FILE.i:149.
@@ -106,7 +96,6 @@ PROJECT_FILE.i:148:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_com
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:150.
-PROJECT_FILE.i:150:[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:151.
@@ -120,46 +109,40 @@ PROJECT_FILE.i:150:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:152.
-PROJECT_FILE.i:152:[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:152.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:153.
-PROJECT_FILE.i:153:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:156:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:159.
-PROJECT_FILE.i:159:[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:159.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:160.
-PROJECT_FILE.i:160:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_add <-main.
         Called from PROJECT_FILE.i:160.
-PROJECT_FILE.i:160:[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_init_set_si <-main.
         Called from PROJECT_FILE.i:161.
-PROJECT_FILE.i:161:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:161.
-PROJECT_FILE.i:161:[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:162.
-PROJECT_FILE.i:162:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:163.
-PROJECT_FILE.i:163:[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:164.
@@ -173,53 +156,46 @@ PROJECT_FILE.i:163:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:165.
-PROJECT_FILE.i:165:[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:165.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:166.
-PROJECT_FILE.i:166:[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:166.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:167.
-PROJECT_FILE.i:167:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:170:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:173.
-PROJECT_FILE.i:173:[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:173.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:174.
-PROJECT_FILE.i:174:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_sub <-main.
         Called from PROJECT_FILE.i:174.
-PROJECT_FILE.i:174:[value] Function mpz_sub: precondition got status valid
+PROJECT_FILE.i:66:[value] Function mpz_sub: precondition got status valid
+PROJECT_FILE.i:67:[value] Function mpz_sub: precondition got status valid
+PROJECT_FILE.i:68:[value] Function mpz_sub: precondition got status valid
 [value] Done for function mpz_sub
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:175.
-PROJECT_FILE.i:175:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:175.
-PROJECT_FILE.i:175:[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:176.
-PROJECT_FILE.i:176:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:177.
-PROJECT_FILE.i:177:[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:178.
@@ -233,53 +209,46 @@ PROJECT_FILE.i:177:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:179.
-PROJECT_FILE.i:179:[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:179.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:180.
-PROJECT_FILE.i:180:[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:180.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:181.
-PROJECT_FILE.i:181:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:184:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:187.
-PROJECT_FILE.i:187:[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:187.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:188.
-PROJECT_FILE.i:188:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_mul <-main.
         Called from PROJECT_FILE.i:188.
-PROJECT_FILE.i:188:[value] Function mpz_mul: precondition got status valid
+PROJECT_FILE.i:72:[value] Function mpz_mul: precondition got status valid
+PROJECT_FILE.i:73:[value] Function mpz_mul: precondition got status valid
+PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid
 [value] Done for function mpz_mul
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:189.
-PROJECT_FILE.i:189:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:189.
-PROJECT_FILE.i:189:[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:190.
-PROJECT_FILE.i:190:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:191.
-PROJECT_FILE.i:191:[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:192.
@@ -293,53 +262,46 @@ PROJECT_FILE.i:191:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:193.
-PROJECT_FILE.i:193:[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:193.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:194.
-PROJECT_FILE.i:194:[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:194.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:195.
-PROJECT_FILE.i:195:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:198:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:201.
-PROJECT_FILE.i:201:[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:201.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:202.
-PROJECT_FILE.i:202:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_cdiv_q <-main.
         Called from PROJECT_FILE.i:203.
-PROJECT_FILE.i:203:[value] Function mpz_cdiv_q: precondition got status valid
+PROJECT_FILE.i:78:[value] Function mpz_cdiv_q: precondition got status valid
+PROJECT_FILE.i:79:[value] Function mpz_cdiv_q: precondition got status valid
+PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid
 [value] Done for function mpz_cdiv_q
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:204.
-PROJECT_FILE.i:204:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:204.
-PROJECT_FILE.i:204:[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:205.
-PROJECT_FILE.i:205:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:206.
-PROJECT_FILE.i:206:[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:207.
@@ -353,53 +315,46 @@ PROJECT_FILE.i:206:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:208.
-PROJECT_FILE.i:208:[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:208.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:209.
-PROJECT_FILE.i:209:[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:209.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:210.
-PROJECT_FILE.i:210:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:213:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:216.
-PROJECT_FILE.i:216:[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:216.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:217.
-PROJECT_FILE.i:217:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_mod <-main.
         Called from PROJECT_FILE.i:217.
-PROJECT_FILE.i:217:[value] Function mpz_mod: precondition got status valid
+PROJECT_FILE.i:84:[value] Function mpz_mod: precondition got status valid
+PROJECT_FILE.i:85:[value] Function mpz_mod: precondition got status valid
+PROJECT_FILE.i:86:[value] Function mpz_mod: precondition got status valid
 [value] Done for function mpz_mod
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:218.
-PROJECT_FILE.i:218:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:218.
-PROJECT_FILE.i:218:[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:219.
-PROJECT_FILE.i:219:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:220.
-PROJECT_FILE.i:220:[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:221.
@@ -413,112 +368,88 @@ PROJECT_FILE.i:220:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:222.
-PROJECT_FILE.i:222:[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:222.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:223.
-PROJECT_FILE.i:223:[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:223.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:224.
-PROJECT_FILE.i:224:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:227:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:233.
-PROJECT_FILE.i:233:[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:234.
-PROJECT_FILE.i:234:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:234.
-PROJECT_FILE.i:234:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_mul <-main.
         Called from PROJECT_FILE.i:235.
-PROJECT_FILE.i:235:[value] Function mpz_mul: precondition got status valid
 [value] Done for function mpz_mul
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:236.
-PROJECT_FILE.i:236:[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:236.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:237.
-PROJECT_FILE.i:237:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_add <-main.
         Called from PROJECT_FILE.i:237.
-PROJECT_FILE.i:237:[value] Function mpz_add: precondition got status valid
 [value] Done for function mpz_add
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:238.
-PROJECT_FILE.i:238:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_add <-main.
         Called from PROJECT_FILE.i:238.
-PROJECT_FILE.i:238:[value] Function mpz_add: precondition got status valid
 [value] Done for function mpz_add
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:239.
-PROJECT_FILE.i:239:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:239.
-PROJECT_FILE.i:239:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_sub <-main.
         Called from PROJECT_FILE.i:240.
-PROJECT_FILE.i:240:[value] Function mpz_sub: precondition got status valid
 [value] Done for function mpz_sub
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:241.
-PROJECT_FILE.i:241:[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:241.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:242.
-PROJECT_FILE.i:242:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_sub <-main.
         Called from PROJECT_FILE.i:243.
-PROJECT_FILE.i:243:[value] Function mpz_sub: precondition got status valid
 [value] Done for function mpz_sub
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:244.
-PROJECT_FILE.i:244:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
 [value] computing for function mpz_add <-main.
         Called from PROJECT_FILE.i:245.
-PROJECT_FILE.i:245:[value] Function mpz_add: precondition got status valid
 [value] Done for function mpz_add
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:246.
-PROJECT_FILE.i:246:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:246.
-PROJECT_FILE.i:246:[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:247.
-PROJECT_FILE.i:247:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:248.
-PROJECT_FILE.i:248:[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:249.
@@ -532,79 +463,67 @@ PROJECT_FILE.i:248:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:250.
-PROJECT_FILE.i:250:[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:250.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:251.
-PROJECT_FILE.i:251:[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:251.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:252.
-PROJECT_FILE.i:252:[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:252.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:253.
-PROJECT_FILE.i:253:[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:253.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:254.
-PROJECT_FILE.i:254:[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:254.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:255.
-PROJECT_FILE.i:255:[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:255.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:256.
-PROJECT_FILE.i:256:[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:256.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:257.
-PROJECT_FILE.i:257:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:260:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:263.
-PROJECT_FILE.i:263:[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:263.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:264.
-PROJECT_FILE.i:264:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:265.
-PROJECT_FILE.i:265:[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:265.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:266.
-PROJECT_FILE.i:266:[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:268.
@@ -618,14 +537,12 @@ PROJECT_FILE.i:266:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:269.
-PROJECT_FILE.i:269:[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:269.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:270.
-PROJECT_FILE.i:270:[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:270.
@@ -633,34 +550,27 @@ PROJECT_FILE.i:270:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:273:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:276.
-PROJECT_FILE.i:276:[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:277.
-PROJECT_FILE.i:277:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:277.
-PROJECT_FILE.i:277:[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:278.
-PROJECT_FILE.i:278:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:279.
-PROJECT_FILE.i:279:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:280.
-PROJECT_FILE.i:280:[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:280.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:281.
-PROJECT_FILE.i:281:[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:283.
@@ -674,53 +584,43 @@ PROJECT_FILE.i:281:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:284.
-PROJECT_FILE.i:284:[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:284.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:285.
-PROJECT_FILE.i:285:[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:285.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:286.
-PROJECT_FILE.i:286:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:289:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:292.
-PROJECT_FILE.i:292:[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:293.
-PROJECT_FILE.i:293:[value] Function mpz_init_set_si: postcondition got status unknown
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE.i:293.
-PROJECT_FILE.i:293:[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:294.
-PROJECT_FILE.i:294:[value] Function mpz_neg: precondition got status valid
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:295.
-PROJECT_FILE.i:295:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:296.
-PROJECT_FILE.i:296:[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:296.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:297.
-PROJECT_FILE.i:297:[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:299.
@@ -734,44 +634,37 @@ PROJECT_FILE.i:297:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:300.
-PROJECT_FILE.i:300:[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:300.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:301.
-PROJECT_FILE.i:301:[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:301.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:302.
-PROJECT_FILE.i:302:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
 PROJECT_FILE.i:305:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:308.
-PROJECT_FILE.i:308:[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:308.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:309.
-PROJECT_FILE.i:309:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:310.
-PROJECT_FILE.i:310:[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:310.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:311.
-PROJECT_FILE.i:311:[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:313.
@@ -785,14 +678,12 @@ PROJECT_FILE.i:311:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:314.
-PROJECT_FILE.i:314:[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:314.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:315.
-PROJECT_FILE.i:315:[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:315.
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 668d1cda588f9a41aa81c31847968d34ee249834..c680c528f34a2352eb89d3bd7f9fec2a0662aa9d 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,14 +7,15 @@ PROJECT_FILE.i:127:[value] Assertion got status valid.
 PROJECT_FILE.i:130:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:132.
-PROJECT_FILE.i:132:[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:132.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:133.
-PROJECT_FILE.i:133:[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:134.
@@ -23,13 +24,13 @@ PROJECT_FILE.i:133:[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:115.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:105:[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:135.
-PROJECT_FILE.i:135:[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:135.
@@ -37,14 +38,12 @@ PROJECT_FILE.i:135:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:138:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:140.
-PROJECT_FILE.i:140:[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:140.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:141.
-PROJECT_FILE.i:141:[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:142.
@@ -58,7 +57,6 @@ PROJECT_FILE.i:141:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:143.
-PROJECT_FILE.i:143:[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:143.
@@ -68,14 +66,12 @@ PROJECT_FILE.i:150:[value] Assertion got status valid.
 PROJECT_FILE.i:153:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:155.
-PROJECT_FILE.i:155:[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:155.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:156.
-PROJECT_FILE.i:156:[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:157.
@@ -89,7 +85,6 @@ PROJECT_FILE.i:156:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:158.
-PROJECT_FILE.i:158:[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:158.
@@ -97,14 +92,12 @@ PROJECT_FILE.i:158:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:161:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:163.
-PROJECT_FILE.i:163:[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:163.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:164.
-PROJECT_FILE.i:164:[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:165.
@@ -118,7 +111,6 @@ PROJECT_FILE.i:164:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:166.
-PROJECT_FILE.i:166:[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:166.
@@ -126,14 +118,12 @@ PROJECT_FILE.i:166:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:169:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:171.
-PROJECT_FILE.i:171:[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:171.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:172.
-PROJECT_FILE.i:172:[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:173.
@@ -147,7 +137,6 @@ PROJECT_FILE.i:172:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:174.
-PROJECT_FILE.i:174:[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:174.
@@ -155,14 +144,12 @@ PROJECT_FILE.i:174:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:177:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:179.
-PROJECT_FILE.i:179:[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:179.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:180.
-PROJECT_FILE.i:180:[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:181.
@@ -176,7 +163,6 @@ PROJECT_FILE.i:180:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:182.
-PROJECT_FILE.i:182:[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:182.
@@ -184,14 +170,12 @@ PROJECT_FILE.i:182:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:185:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:187.
-PROJECT_FILE.i:187:[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:187.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:188.
-PROJECT_FILE.i:188:[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:189.
@@ -205,7 +189,6 @@ PROJECT_FILE.i:188:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:190.
-PROJECT_FILE.i:190:[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:190.
@@ -213,14 +196,12 @@ PROJECT_FILE.i:190:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:193:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:195.
-PROJECT_FILE.i:195:[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:195.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:196.
-PROJECT_FILE.i:196:[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:197.
@@ -234,7 +215,6 @@ PROJECT_FILE.i:196:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:198.
-PROJECT_FILE.i:198:[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:198.
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 d9645140f4cd9fa938d6943834eaf3321fb7ed07..7a671a099b2849b5fde1e6733b0b752232206cc7 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
@@ -5,14 +5,15 @@
 PROJECT_FILE.i:119:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:121.
-PROJECT_FILE.i:121:[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:121.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:122.
-PROJECT_FILE.i:122:[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:123.
@@ -21,13 +22,13 @@ PROJECT_FILE.i:122:[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:115.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:105:[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:124.
-PROJECT_FILE.i:124:[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:124.
@@ -35,14 +36,12 @@ PROJECT_FILE.i:124:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:127:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <-main.
         Called from PROJECT_FILE.i:129.
-PROJECT_FILE.i:129:[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:129.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:130.
-PROJECT_FILE.i:130:[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:131.
@@ -56,7 +55,6 @@ PROJECT_FILE.i:130:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:132.
-PROJECT_FILE.i:132:[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:132.
@@ -64,15 +62,13 @@ PROJECT_FILE.i:132:[value] Function mpz_clear: precondition got status valid
 PROJECT_FILE.i:135:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_str <-main.
         Called from PROJECT_FILE.i:137.
-PROJECT_FILE.i:137:[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:138.
-PROJECT_FILE.i:138:[value] Function mpz_init_set_str: postcondition got status unknown
 [value] Done for function mpz_init_set_str
 [value] computing for function mpz_cmp <-main.
         Called from PROJECT_FILE.i:139.
-PROJECT_FILE.i:139:[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.
@@ -86,7 +82,6 @@ PROJECT_FILE.i:139:[value] Function mpz_cmp: precondition got status valid
 [value] Done for function e_acsl_fail
 [value] computing for function mpz_clear <-main.
         Called from PROJECT_FILE.i:142.
-PROJECT_FILE.i:142:[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.