diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 515f1b1b5b7f708f1ddb61cbab1f032e33e36700..6e25b3352399d1e533faade540db581975c927e4 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -13,6 +13,8 @@ the plug-in would generate something like
 /*@ assert \forall integer x; -1<= x<= 1 ==>  (x != 0&&  1/x == 0) || (x != 0
 &&  1/x != 0); */ 
 
+- pour ces gardes, aussi générer une annotation acsl correspondante (?)
+
 - mkcall ne devrait pas générer de nouvelles variables pour une même fonction
 
 [TODO?] mettre des locations intelligentes
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 69fdc5c217b22c0eebfd739016aacd0e3dddb422..d3c9b30597e7c54fa3950d6c8e1bd2e2a67982e4 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
@@ -10,7 +10,7 @@ PROJECT_FILE.i:123:[value] Assertion got status valid.
 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.
+        Called from PROJECT_FILE.i:125.
 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.
@@ -19,15 +19,15 @@ 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.
+        Called from PROJECT_FILE.i:126.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:128.
+        Called from PROJECT_FILE.i:127.
 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.
+        Called from PROJECT_FILE.i:128.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -38,33 +38,33 @@ PROJECT_FILE.i:105:[value] Function exit: postcondition got status invalid
 [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.
+        Called from PROJECT_FILE.i:128.
 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.
+        Called from PROJECT_FILE.i:129.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:131.
+        Called from PROJECT_FILE.i:129.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:134:[value] Assertion got status valid.
+PROJECT_FILE.i:132:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:136.
+        Called from PROJECT_FILE.i:134.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:137.
+        Called from PROJECT_FILE.i:134.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:137.
+        Called from PROJECT_FILE.i:135.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:138.
+        Called from PROJECT_FILE.i:135.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:139.
+        Called from PROJECT_FILE.i:136.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:140.
+        Called from PROJECT_FILE.i:137.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -74,33 +74,33 @@ PROJECT_FILE.i:134:[value] Assertion got status valid.
 [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:141.
+        Called from PROJECT_FILE.i:137.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:141.
+        Called from PROJECT_FILE.i:138.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:142.
+        Called from PROJECT_FILE.i:138.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:145:[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:147.
+        Called from PROJECT_FILE.i:143.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:148.
+        Called from PROJECT_FILE.i:143.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:148.
+        Called from PROJECT_FILE.i:144.
 [value] Done for function mpz_init
 [value] computing for function mpz_com <- main.
-        Called from PROJECT_FILE.i:149.
+        Called from PROJECT_FILE.i:144.
 [kernel] warning: No code for function mpz_com, default assigns generated
 [value] Done for function mpz_com
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:150.
+        Called from PROJECT_FILE.i:145.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:151.
+        Called from PROJECT_FILE.i:146.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -110,44 +110,44 @@ PROJECT_FILE.i:145:[value] Assertion got status valid.
 [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:152.
+        Called from PROJECT_FILE.i:146.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:152.
+        Called from PROJECT_FILE.i:147.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:153.
+        Called from PROJECT_FILE.i:147.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:156:[value] Assertion got status valid.
+PROJECT_FILE.i:150:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:159.
+        Called from PROJECT_FILE.i:152.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:159.
+        Called from PROJECT_FILE.i:153.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:160.
+        Called from PROJECT_FILE.i:153.
 [value] Done for function mpz_init
 [value] computing for function mpz_add <- main.
-        Called from PROJECT_FILE.i:160.
+        Called from PROJECT_FILE.i:154.
 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.
+        Called from PROJECT_FILE.i:154.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:161.
+        Called from PROJECT_FILE.i:155.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:162.
+        Called from PROJECT_FILE.i:155.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:163.
+        Called from PROJECT_FILE.i:156.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:164.
+        Called from PROJECT_FILE.i:157.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -157,50 +157,50 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
 [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:165.
+        Called from PROJECT_FILE.i:157.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:165.
+        Called from PROJECT_FILE.i:158.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:166.
+        Called from PROJECT_FILE.i:158.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:166.
+        Called from PROJECT_FILE.i:158.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:167.
+        Called from PROJECT_FILE.i:159.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:170:[value] Assertion got status valid.
+PROJECT_FILE.i:162:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:173.
+        Called from PROJECT_FILE.i:164.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:173.
+        Called from PROJECT_FILE.i:165.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:174.
+        Called from PROJECT_FILE.i:165.
 [value] Done for function mpz_init
 [value] computing for function mpz_sub <- main.
-        Called from PROJECT_FILE.i:174.
+        Called from PROJECT_FILE.i:166.
 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.
+        Called from PROJECT_FILE.i:166.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:175.
+        Called from PROJECT_FILE.i:167.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:176.
+        Called from PROJECT_FILE.i:167.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:177.
+        Called from PROJECT_FILE.i:168.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:178.
+        Called from PROJECT_FILE.i:169.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -210,50 +210,50 @@ PROJECT_FILE.i:68:[value] Function mpz_sub: precondition got status valid
 [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:179.
+        Called from PROJECT_FILE.i:169.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:179.
+        Called from PROJECT_FILE.i:170.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:180.
+        Called from PROJECT_FILE.i:170.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:180.
+        Called from PROJECT_FILE.i:170.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:181.
+        Called from PROJECT_FILE.i:171.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:184:[value] Assertion got status valid.
+PROJECT_FILE.i:174:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:187.
+        Called from PROJECT_FILE.i:176.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:187.
+        Called from PROJECT_FILE.i:177.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:188.
+        Called from PROJECT_FILE.i:177.
 [value] Done for function mpz_init
 [value] computing for function mpz_mul <- main.
-        Called from PROJECT_FILE.i:188.
+        Called from PROJECT_FILE.i:178.
 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.
+        Called from PROJECT_FILE.i:178.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:189.
+        Called from PROJECT_FILE.i:179.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:190.
+        Called from PROJECT_FILE.i:179.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:191.
+        Called from PROJECT_FILE.i:180.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:192.
+        Called from PROJECT_FILE.i:181.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -263,50 +263,50 @@ PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid
 [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:193.
+        Called from PROJECT_FILE.i:181.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:182.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:194.
+        Called from PROJECT_FILE.i:182.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:194.
+        Called from PROJECT_FILE.i:182.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:195.
+        Called from PROJECT_FILE.i:183.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:198:[value] Assertion got status valid.
+PROJECT_FILE.i:186:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:201.
+        Called from PROJECT_FILE.i:188.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:201.
+        Called from PROJECT_FILE.i:189.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:202.
+        Called from PROJECT_FILE.i:189.
 [value] Done for function mpz_init
 [value] computing for function mpz_cdiv_q <- main.
-        Called from PROJECT_FILE.i:203.
+        Called from PROJECT_FILE.i:190.
 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.
+        Called from PROJECT_FILE.i:190.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:204.
+        Called from PROJECT_FILE.i:191.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:205.
+        Called from PROJECT_FILE.i:191.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:206.
+        Called from PROJECT_FILE.i:192.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:207.
+        Called from PROJECT_FILE.i:193.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -316,50 +316,50 @@ PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid
 [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:208.
+        Called from PROJECT_FILE.i:193.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:208.
+        Called from PROJECT_FILE.i:194.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:209.
+        Called from PROJECT_FILE.i:194.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:209.
+        Called from PROJECT_FILE.i:194.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:210.
+        Called from PROJECT_FILE.i:195.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:213:[value] Assertion got status valid.
+PROJECT_FILE.i:198:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:216.
+        Called from PROJECT_FILE.i:200.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:216.
+        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:217.
+        Called from PROJECT_FILE.i:201.
 [value] Done for function mpz_init
 [value] computing for function mpz_mod <- main.
-        Called from PROJECT_FILE.i:217.
+        Called from PROJECT_FILE.i:202.
 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.
+        Called from PROJECT_FILE.i:202.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:218.
+        Called from PROJECT_FILE.i:203.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:219.
+        Called from PROJECT_FILE.i:203.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:220.
+        Called from PROJECT_FILE.i:204.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:221.
+        Called from PROJECT_FILE.i:205.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -369,92 +369,92 @@ PROJECT_FILE.i:86:[value] Function mpz_mod: precondition got status valid
 [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:222.
+        Called from PROJECT_FILE.i:205.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:222.
+        Called from PROJECT_FILE.i:206.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:223.
+        Called from PROJECT_FILE.i:206.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:223.
+        Called from PROJECT_FILE.i:206.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:224.
+        Called from PROJECT_FILE.i:207.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:227:[value] Assertion got status valid.
+PROJECT_FILE.i:210:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:233.
+        Called from PROJECT_FILE.i:215.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:234.
+        Called from PROJECT_FILE.i:215.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:234.
+        Called from PROJECT_FILE.i:216.
 [value] Done for function mpz_init
 [value] computing for function mpz_mul <- main.
-        Called from PROJECT_FILE.i:235.
+        Called from PROJECT_FILE.i:216.
 [value] Done for function mpz_mul
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:236.
+        Called from PROJECT_FILE.i:217.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:236.
+        Called from PROJECT_FILE.i:217.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:237.
+        Called from PROJECT_FILE.i:218.
 [value] Done for function mpz_init
 [value] computing for function mpz_add <- main.
-        Called from PROJECT_FILE.i:237.
+        Called from PROJECT_FILE.i:218.
 [value] Done for function mpz_add
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:238.
+        Called from PROJECT_FILE.i:219.
 [value] Done for function mpz_init
 [value] computing for function mpz_add <- main.
-        Called from PROJECT_FILE.i:238.
+        Called from PROJECT_FILE.i:219.
 [value] Done for function mpz_add
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:239.
+        Called from PROJECT_FILE.i:220.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:239.
+        Called from PROJECT_FILE.i:220.
 [value] Done for function mpz_init
 [value] computing for function mpz_sub <- main.
-        Called from PROJECT_FILE.i:240.
+        Called from PROJECT_FILE.i:221.
 [value] Done for function mpz_sub
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:241.
+        Called from PROJECT_FILE.i:221.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:241.
+        Called from PROJECT_FILE.i:222.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:242.
+        Called from PROJECT_FILE.i:222.
 [value] Done for function mpz_init
 [value] computing for function mpz_sub <- main.
-        Called from PROJECT_FILE.i:243.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function mpz_sub
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:244.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function mpz_init
 [value] computing for function mpz_add <- main.
-        Called from PROJECT_FILE.i:245.
+        Called from PROJECT_FILE.i:224.
 [value] Done for function mpz_add
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:246.
+        Called from PROJECT_FILE.i:224.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:246.
+        Called from PROJECT_FILE.i:225.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:247.
+        Called from PROJECT_FILE.i:225.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:248.
+        Called from PROJECT_FILE.i:226.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:249.
+        Called from PROJECT_FILE.i:227.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -464,71 +464,71 @@ PROJECT_FILE.i:227:[value] Assertion got status valid.
 [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:250.
+        Called from PROJECT_FILE.i:228.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:250.
+        Called from PROJECT_FILE.i:228.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:251.
+        Called from PROJECT_FILE.i:228.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:251.
+        Called from PROJECT_FILE.i:229.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:252.
+        Called from PROJECT_FILE.i:229.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:252.
+        Called from PROJECT_FILE.i:229.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:253.
+        Called from PROJECT_FILE.i:230.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:253.
+        Called from PROJECT_FILE.i:230.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:254.
+        Called from PROJECT_FILE.i:230.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:254.
+        Called from PROJECT_FILE.i:231.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:255.
+        Called from PROJECT_FILE.i:231.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:255.
+        Called from PROJECT_FILE.i:231.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:256.
+        Called from PROJECT_FILE.i:232.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:256.
+        Called from PROJECT_FILE.i:232.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:257.
+        Called from PROJECT_FILE.i:232.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:260:[value] Assertion got status valid.
+PROJECT_FILE.i:235:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:263.
+        Called from PROJECT_FILE.i:237.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:263.
+        Called from PROJECT_FILE.i:238.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:264.
+        Called from PROJECT_FILE.i:238.
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:265.
+        Called from PROJECT_FILE.i:239.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:265.
+        Called from PROJECT_FILE.i:239.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:266.
+        Called from PROJECT_FILE.i:240.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:268.
+        Called from PROJECT_FILE.i:242.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -538,44 +538,44 @@ PROJECT_FILE.i:260:[value] Assertion got status valid.
 [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:269.
+        Called from PROJECT_FILE.i:243.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:269.
+        Called from PROJECT_FILE.i:243.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:270.
+        Called from PROJECT_FILE.i:243.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:270.
+        Called from PROJECT_FILE.i:244.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:273:[value] Assertion got status valid.
+PROJECT_FILE.i:247:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:276.
+        Called from PROJECT_FILE.i:250.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:277.
+        Called from PROJECT_FILE.i:250.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:277.
+        Called from PROJECT_FILE.i:251.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:278.
+        Called from PROJECT_FILE.i:251.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:279.
+        Called from PROJECT_FILE.i:252.
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:280.
+        Called from PROJECT_FILE.i:252.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:280.
+        Called from PROJECT_FILE.i:253.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:281.
+        Called from PROJECT_FILE.i:253.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:283.
+        Called from PROJECT_FILE.i:255.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -585,47 +585,47 @@ PROJECT_FILE.i:273:[value] Assertion got status valid.
 [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:284.
+        Called from PROJECT_FILE.i:256.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:284.
+        Called from PROJECT_FILE.i:256.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:285.
+        Called from PROJECT_FILE.i:256.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:285.
+        Called from PROJECT_FILE.i:257.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:286.
+        Called from PROJECT_FILE.i:257.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:289:[value] Assertion got status valid.
+PROJECT_FILE.i:260:[value] Assertion got status valid.
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:292.
+        Called from PROJECT_FILE.i:263.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:293.
+        Called from PROJECT_FILE.i:263.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init <- main.
-        Called from PROJECT_FILE.i:293.
+        Called from PROJECT_FILE.i:264.
 [value] Done for function mpz_init
 [value] computing for function mpz_neg <- main.
-        Called from PROJECT_FILE.i:294.
+        Called from PROJECT_FILE.i:264.
 [value] Done for function mpz_neg
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:295.
+        Called from PROJECT_FILE.i:265.
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:296.
+        Called from PROJECT_FILE.i:265.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:296.
+        Called from PROJECT_FILE.i:266.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:297.
+        Called from PROJECT_FILE.i:266.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:299.
+        Called from PROJECT_FILE.i:268.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -635,41 +635,41 @@ PROJECT_FILE.i:289:[value] Assertion got status valid.
 [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:300.
+        Called from PROJECT_FILE.i:269.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:300.
+        Called from PROJECT_FILE.i:269.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:301.
+        Called from PROJECT_FILE.i:269.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:301.
+        Called from PROJECT_FILE.i:270.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:302.
+        Called from PROJECT_FILE.i:270.
 [value] Done for function mpz_clear
-PROJECT_FILE.i:305:[value] Assertion 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:308.
+        Called from PROJECT_FILE.i:275.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:308.
+        Called from PROJECT_FILE.i:276.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:309.
+        Called from PROJECT_FILE.i:276.
 [value] Done for function mpz_cmp
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:310.
+        Called from PROJECT_FILE.i:277.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:310.
+        Called from PROJECT_FILE.i:277.
 [value] Done for function mpz_init_set_si
 [value] computing for function mpz_cmp <- main.
-        Called from PROJECT_FILE.i:311.
+        Called from PROJECT_FILE.i:278.
 [value] Done for function mpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:313.
+        Called from PROJECT_FILE.i:280.
 [value] computing for function printf <- e_acsl_fail <- main.
         Called from PROJECT_FILE.i:115.
 [value] Done for function printf
@@ -679,16 +679,16 @@ PROJECT_FILE.i:305:[value] Assertion got status valid.
 [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:314.
+        Called from PROJECT_FILE.i:281.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:314.
+        Called from PROJECT_FILE.i:281.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:315.
+        Called from PROJECT_FILE.i:281.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
-        Called from PROJECT_FILE.i:315.
+        Called from PROJECT_FILE.i:282.
 [value] Done for function mpz_clear
 [value] Recording results for main
 [value] done for function main
@@ -820,314 +820,285 @@ void main(void)
   x = -3;
   y = 2;
   /*@ assert -3 ≡ x; */ ;
-  { mpz_t e_acsl_cst_1; mpz_t e_acsl_cst_2; mpz_t e_acsl_cst_3;
-    int e_acsl_cst_4;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long)3);
-    mpz_init((__mpz_struct *)(e_acsl_cst_2));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_2),
-            (__mpz_struct const *)(e_acsl_cst_1));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_3),(long)x);
-    e_acsl_cst_4 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_2),
-                           (__mpz_struct const *)(e_acsl_cst_3));
-    if (e_acsl_cst_4 != 0) { e_acsl_fail((char *)"(-3 == x)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_1));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_2));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_3));
+  { mpz_t e_acsl_1; mpz_t e_acsl_2; mpz_t e_acsl_3; int e_acsl_4;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)3);
+    mpz_init((__mpz_struct *)(e_acsl_2));
+    mpz_neg((__mpz_struct *)(e_acsl_2),(__mpz_struct const *)(e_acsl_1));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_3),(long)x);
+    e_acsl_4 = mpz_cmp((__mpz_struct const *)(e_acsl_2),
+                       (__mpz_struct const *)(e_acsl_3));
+    if (e_acsl_4 != 0) { e_acsl_fail((char *)"(-3 == x)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_1));
+    mpz_clear((__mpz_struct *)(e_acsl_2));
+    mpz_clear((__mpz_struct *)(e_acsl_3));
   }
   
   /*@ assert x ≡ -3; */ ;
-  { mpz_t e_acsl_cst_5; mpz_t e_acsl_cst_6; mpz_t e_acsl_cst_7;
-    int e_acsl_cst_8;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_6),(long)3);
-    mpz_init((__mpz_struct *)(e_acsl_cst_7));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_7),
-            (__mpz_struct const *)(e_acsl_cst_6));
-    e_acsl_cst_8 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_5),
-                           (__mpz_struct const *)(e_acsl_cst_7));
-    if (e_acsl_cst_8 != 0) { e_acsl_fail((char *)"(x == -3)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_5));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_6));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_7));
+  { mpz_t e_acsl_5; mpz_t e_acsl_6; mpz_t e_acsl_7; int e_acsl_8;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_6),(long)3);
+    mpz_init((__mpz_struct *)(e_acsl_7));
+    mpz_neg((__mpz_struct *)(e_acsl_7),(__mpz_struct const *)(e_acsl_6));
+    e_acsl_8 = mpz_cmp((__mpz_struct const *)(e_acsl_5),
+                       (__mpz_struct const *)(e_acsl_7));
+    if (e_acsl_8 != 0) { e_acsl_fail((char *)"(x == -3)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_5));
+    mpz_clear((__mpz_struct *)(e_acsl_6));
+    mpz_clear((__mpz_struct *)(e_acsl_7));
   }
   
   /*@ assert 0 ≢ ~0; */ ;
-  { mpz_t e_acsl_cst_9; mpz_t e_acsl_cst_10; mpz_t e_acsl_cst_11;
-    int e_acsl_cst_12;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_9),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_10),(long)0);
-    mpz_init((__mpz_struct *)(e_acsl_cst_11));
-    mpz_com(e_acsl_cst_11,e_acsl_cst_10);
-    e_acsl_cst_12 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_9),
-                            (__mpz_struct const *)(e_acsl_cst_11));
-    if (e_acsl_cst_12 == 0) { e_acsl_fail((char *)"(0 != ~0)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_9));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_10));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_11));
+  { mpz_t e_acsl_9; mpz_t e_acsl_10; mpz_t e_acsl_11; int e_acsl_12;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)0);
+    mpz_init((__mpz_struct *)(e_acsl_11)); mpz_com(e_acsl_11,e_acsl_10);
+    e_acsl_12 = mpz_cmp((__mpz_struct const *)(e_acsl_9),
+                        (__mpz_struct const *)(e_acsl_11));
+    if (e_acsl_12 == 0) { e_acsl_fail((char *)"(0 != ~0)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_9));
+    mpz_clear((__mpz_struct *)(e_acsl_10));
+    mpz_clear((__mpz_struct *)(e_acsl_11));
   }
   
   /*@ assert x+1 ≡ -2; */ ;
-  { mpz_t e_acsl_cst_13; mpz_t e_acsl_cst_14; mpz_t e_acsl_cst_15;
-    mpz_t e_acsl_cst_16; mpz_t e_acsl_cst_17; int e_acsl_cst_18;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_13),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_14),(long)1);
-    mpz_init((__mpz_struct *)(e_acsl_cst_15));
-    mpz_add((__mpz_struct *)(e_acsl_cst_15),
-            (__mpz_struct const *)(e_acsl_cst_13),
-            (__mpz_struct const *)(e_acsl_cst_14));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_16),(long)2);
-    mpz_init((__mpz_struct *)(e_acsl_cst_17));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_17),
-            (__mpz_struct const *)(e_acsl_cst_16));
-    e_acsl_cst_18 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_15),
-                            (__mpz_struct const *)(e_acsl_cst_17));
-    if (e_acsl_cst_18 != 0) { e_acsl_fail((char *)"(x+1 == -2)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_13));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_14));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_15));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_16));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_17));
+  { mpz_t e_acsl_13; mpz_t e_acsl_14; mpz_t e_acsl_15; mpz_t e_acsl_16;
+    mpz_t e_acsl_17; int e_acsl_18;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_13),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)1);
+    mpz_init((__mpz_struct *)(e_acsl_15));
+    mpz_add((__mpz_struct *)(e_acsl_15),(__mpz_struct const *)(e_acsl_13),
+            (__mpz_struct const *)(e_acsl_14));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)2);
+    mpz_init((__mpz_struct *)(e_acsl_17));
+    mpz_neg((__mpz_struct *)(e_acsl_17),(__mpz_struct const *)(e_acsl_16));
+    e_acsl_18 = mpz_cmp((__mpz_struct const *)(e_acsl_15),
+                        (__mpz_struct const *)(e_acsl_17));
+    if (e_acsl_18 != 0) { e_acsl_fail((char *)"(x+1 == -2)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_13));
+    mpz_clear((__mpz_struct *)(e_acsl_14));
+    mpz_clear((__mpz_struct *)(e_acsl_15));
+    mpz_clear((__mpz_struct *)(e_acsl_16));
+    mpz_clear((__mpz_struct *)(e_acsl_17));
   }
   
   /*@ assert x-1 ≡ -4; */ ;
-  { mpz_t e_acsl_cst_19; mpz_t e_acsl_cst_20; mpz_t e_acsl_cst_21;
-    mpz_t e_acsl_cst_22; mpz_t e_acsl_cst_23; int e_acsl_cst_24;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_19),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_20),(long)1);
-    mpz_init((__mpz_struct *)(e_acsl_cst_21));
-    mpz_sub((__mpz_struct *)(e_acsl_cst_21),
-            (__mpz_struct const *)(e_acsl_cst_19),
-            (__mpz_struct const *)(e_acsl_cst_20));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_22),(long)4);
-    mpz_init((__mpz_struct *)(e_acsl_cst_23));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_23),
-            (__mpz_struct const *)(e_acsl_cst_22));
-    e_acsl_cst_24 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_21),
-                            (__mpz_struct const *)(e_acsl_cst_23));
-    if (e_acsl_cst_24 != 0) { e_acsl_fail((char *)"(x-1 == -4)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_19));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_20));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_21));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_22));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_23));
+  { mpz_t e_acsl_19; mpz_t e_acsl_20; mpz_t e_acsl_21; mpz_t e_acsl_22;
+    mpz_t e_acsl_23; int e_acsl_24;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)1);
+    mpz_init((__mpz_struct *)(e_acsl_21));
+    mpz_sub((__mpz_struct *)(e_acsl_21),(__mpz_struct const *)(e_acsl_19),
+            (__mpz_struct const *)(e_acsl_20));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)4);
+    mpz_init((__mpz_struct *)(e_acsl_23));
+    mpz_neg((__mpz_struct *)(e_acsl_23),(__mpz_struct const *)(e_acsl_22));
+    e_acsl_24 = mpz_cmp((__mpz_struct const *)(e_acsl_21),
+                        (__mpz_struct const *)(e_acsl_23));
+    if (e_acsl_24 != 0) { e_acsl_fail((char *)"(x-1 == -4)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_19));
+    mpz_clear((__mpz_struct *)(e_acsl_20));
+    mpz_clear((__mpz_struct *)(e_acsl_21));
+    mpz_clear((__mpz_struct *)(e_acsl_22));
+    mpz_clear((__mpz_struct *)(e_acsl_23));
   }
   
   /*@ assert x*3 ≡ -9; */ ;
-  { mpz_t e_acsl_cst_25; mpz_t e_acsl_cst_26; mpz_t e_acsl_cst_27;
-    mpz_t e_acsl_cst_28; mpz_t e_acsl_cst_29; int e_acsl_cst_30;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_25),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_26),(long)3);
-    mpz_init((__mpz_struct *)(e_acsl_cst_27));
-    mpz_mul((__mpz_struct *)(e_acsl_cst_27),
-            (__mpz_struct const *)(e_acsl_cst_25),
-            (__mpz_struct const *)(e_acsl_cst_26));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_28),(long)9);
-    mpz_init((__mpz_struct *)(e_acsl_cst_29));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_29),
-            (__mpz_struct const *)(e_acsl_cst_28));
-    e_acsl_cst_30 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_27),
-                            (__mpz_struct const *)(e_acsl_cst_29));
-    if (e_acsl_cst_30 != 0) { e_acsl_fail((char *)"(x*3 == -9)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_25));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_26));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_27));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_28));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_29));
+  { mpz_t e_acsl_25; mpz_t e_acsl_26; mpz_t e_acsl_27; mpz_t e_acsl_28;
+    mpz_t e_acsl_29; int e_acsl_30;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_25),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)3);
+    mpz_init((__mpz_struct *)(e_acsl_27));
+    mpz_mul((__mpz_struct *)(e_acsl_27),(__mpz_struct const *)(e_acsl_25),
+            (__mpz_struct const *)(e_acsl_26));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_28),(long)9);
+    mpz_init((__mpz_struct *)(e_acsl_29));
+    mpz_neg((__mpz_struct *)(e_acsl_29),(__mpz_struct const *)(e_acsl_28));
+    e_acsl_30 = mpz_cmp((__mpz_struct const *)(e_acsl_27),
+                        (__mpz_struct const *)(e_acsl_29));
+    if (e_acsl_30 != 0) { e_acsl_fail((char *)"(x*3 == -9)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_25));
+    mpz_clear((__mpz_struct *)(e_acsl_26));
+    mpz_clear((__mpz_struct *)(e_acsl_27));
+    mpz_clear((__mpz_struct *)(e_acsl_28));
+    mpz_clear((__mpz_struct *)(e_acsl_29));
   }
   
   /*@ assert x/3 ≡ -1; */ ;
-  { mpz_t e_acsl_cst_31; mpz_t e_acsl_cst_32; mpz_t e_acsl_cst_33;
-    mpz_t e_acsl_cst_34; mpz_t e_acsl_cst_35; int e_acsl_cst_36;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_31),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_32),(long)3);
-    mpz_init((__mpz_struct *)(e_acsl_cst_33));
-    mpz_cdiv_q((__mpz_struct *)(e_acsl_cst_33),
-               (__mpz_struct const *)(e_acsl_cst_31),
-               (__mpz_struct const *)(e_acsl_cst_32));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_34),(long)1);
-    mpz_init((__mpz_struct *)(e_acsl_cst_35));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_35),
-            (__mpz_struct const *)(e_acsl_cst_34));
-    e_acsl_cst_36 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_33),
-                            (__mpz_struct const *)(e_acsl_cst_35));
-    if (e_acsl_cst_36 != 0) { e_acsl_fail((char *)"(x/3 == -1)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_31));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_32));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_33));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_34));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_35));
+  { mpz_t e_acsl_31; mpz_t e_acsl_32; mpz_t e_acsl_33; mpz_t e_acsl_34;
+    mpz_t e_acsl_35; int e_acsl_36;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)3);
+    mpz_init((__mpz_struct *)(e_acsl_33));
+    mpz_cdiv_q((__mpz_struct *)(e_acsl_33),(__mpz_struct const *)(e_acsl_31),
+               (__mpz_struct const *)(e_acsl_32));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)1);
+    mpz_init((__mpz_struct *)(e_acsl_35));
+    mpz_neg((__mpz_struct *)(e_acsl_35),(__mpz_struct const *)(e_acsl_34));
+    e_acsl_36 = mpz_cmp((__mpz_struct const *)(e_acsl_33),
+                        (__mpz_struct const *)(e_acsl_35));
+    if (e_acsl_36 != 0) { e_acsl_fail((char *)"(x/3 == -1)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_31));
+    mpz_clear((__mpz_struct *)(e_acsl_32));
+    mpz_clear((__mpz_struct *)(e_acsl_33));
+    mpz_clear((__mpz_struct *)(e_acsl_34));
+    mpz_clear((__mpz_struct *)(e_acsl_35));
   }
   
   /*@ assert x%2 ≡ -1; */ ;
-  { mpz_t e_acsl_cst_37; mpz_t e_acsl_cst_38; mpz_t e_acsl_cst_39;
-    mpz_t e_acsl_cst_40; mpz_t e_acsl_cst_41; int e_acsl_cst_42;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_37),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_38),(long)2);
-    mpz_init((__mpz_struct *)(e_acsl_cst_39));
-    mpz_mod((__mpz_struct *)(e_acsl_cst_39),
-            (__mpz_struct const *)(e_acsl_cst_37),
-            (__mpz_struct const *)(e_acsl_cst_38));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_40),(long)1);
-    mpz_init((__mpz_struct *)(e_acsl_cst_41));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_41),
-            (__mpz_struct const *)(e_acsl_cst_40));
-    e_acsl_cst_42 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_39),
-                            (__mpz_struct const *)(e_acsl_cst_41));
-    if (e_acsl_cst_42 != 0) { e_acsl_fail((char *)"(x%2 == -1)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_37));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_38));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_39));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_40));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_41));
+  { mpz_t e_acsl_37; mpz_t e_acsl_38; mpz_t e_acsl_39; mpz_t e_acsl_40;
+    mpz_t e_acsl_41; int e_acsl_42;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)2);
+    mpz_init((__mpz_struct *)(e_acsl_39));
+    mpz_mod((__mpz_struct *)(e_acsl_39),(__mpz_struct const *)(e_acsl_37),
+            (__mpz_struct const *)(e_acsl_38));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)1);
+    mpz_init((__mpz_struct *)(e_acsl_41));
+    mpz_neg((__mpz_struct *)(e_acsl_41),(__mpz_struct const *)(e_acsl_40));
+    e_acsl_42 = mpz_cmp((__mpz_struct const *)(e_acsl_39),
+                        (__mpz_struct const *)(e_acsl_41));
+    if (e_acsl_42 != 0) { e_acsl_fail((char *)"(x%2 == -1)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_37));
+    mpz_clear((__mpz_struct *)(e_acsl_38));
+    mpz_clear((__mpz_struct *)(e_acsl_39));
+    mpz_clear((__mpz_struct *)(e_acsl_40));
+    mpz_clear((__mpz_struct *)(e_acsl_41));
   }
   
   /*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */ ;
-  { mpz_t e_acsl_cst_43; mpz_t e_acsl_cst_44; mpz_t e_acsl_cst_45;
-    mpz_t e_acsl_cst_46; mpz_t e_acsl_cst_47; mpz_t e_acsl_cst_48;
-    mpz_t e_acsl_cst_49; mpz_t e_acsl_cst_50; mpz_t e_acsl_cst_51;
-    mpz_t e_acsl_cst_52; mpz_t e_acsl_cst_53; mpz_t e_acsl_cst_54;
-    mpz_t e_acsl_cst_55; mpz_t e_acsl_cst_56; mpz_t e_acsl_cst_57;
-    int e_acsl_cst_58;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_43),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_44),(long)2);
-    mpz_init((__mpz_struct *)(e_acsl_cst_45));
-    mpz_mul((__mpz_struct *)(e_acsl_cst_45),
-            (__mpz_struct const *)(e_acsl_cst_43),
-            (__mpz_struct const *)(e_acsl_cst_44));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_46),(long)3);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_47),(long)y);
-    mpz_init((__mpz_struct *)(e_acsl_cst_48));
-    mpz_add((__mpz_struct *)(e_acsl_cst_48),
-            (__mpz_struct const *)(e_acsl_cst_46),
-            (__mpz_struct const *)(e_acsl_cst_47));
-    mpz_init((__mpz_struct *)(e_acsl_cst_49));
-    mpz_add((__mpz_struct *)(e_acsl_cst_49),
-            (__mpz_struct const *)(e_acsl_cst_45),
-            (__mpz_struct const *)(e_acsl_cst_48));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_50),(long)4);
-    mpz_init((__mpz_struct *)(e_acsl_cst_51));
-    mpz_sub((__mpz_struct *)(e_acsl_cst_51),
-            (__mpz_struct const *)(e_acsl_cst_49),
-            (__mpz_struct const *)(e_acsl_cst_50));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_52),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_53),(long)y);
-    mpz_init((__mpz_struct *)(e_acsl_cst_54));
-    mpz_sub((__mpz_struct *)(e_acsl_cst_54),
-            (__mpz_struct const *)(e_acsl_cst_52),
-            (__mpz_struct const *)(e_acsl_cst_53));
-    mpz_init((__mpz_struct *)(e_acsl_cst_55));
-    mpz_add((__mpz_struct *)(e_acsl_cst_55),
-            (__mpz_struct const *)(e_acsl_cst_51),
-            (__mpz_struct const *)(e_acsl_cst_54));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_56),(long)10);
-    mpz_init((__mpz_struct *)(e_acsl_cst_57));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_57),
-            (__mpz_struct const *)(e_acsl_cst_56));
-    e_acsl_cst_58 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_55),
-                            (__mpz_struct const *)(e_acsl_cst_57));
-    if (e_acsl_cst_58 != 0) {
+  { mpz_t e_acsl_43; mpz_t e_acsl_44; mpz_t e_acsl_45; mpz_t e_acsl_46;
+    mpz_t e_acsl_47; mpz_t e_acsl_48; mpz_t e_acsl_49; mpz_t e_acsl_50;
+    mpz_t e_acsl_51; mpz_t e_acsl_52; mpz_t e_acsl_53; mpz_t e_acsl_54;
+    mpz_t e_acsl_55; mpz_t e_acsl_56; mpz_t e_acsl_57; int e_acsl_58;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_44),(long)2);
+    mpz_init((__mpz_struct *)(e_acsl_45));
+    mpz_mul((__mpz_struct *)(e_acsl_45),(__mpz_struct const *)(e_acsl_43),
+            (__mpz_struct const *)(e_acsl_44));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)3);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_47),(long)y);
+    mpz_init((__mpz_struct *)(e_acsl_48));
+    mpz_add((__mpz_struct *)(e_acsl_48),(__mpz_struct const *)(e_acsl_46),
+            (__mpz_struct const *)(e_acsl_47));
+    mpz_init((__mpz_struct *)(e_acsl_49));
+    mpz_add((__mpz_struct *)(e_acsl_49),(__mpz_struct const *)(e_acsl_45),
+            (__mpz_struct const *)(e_acsl_48));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)4);
+    mpz_init((__mpz_struct *)(e_acsl_51));
+    mpz_sub((__mpz_struct *)(e_acsl_51),(__mpz_struct const *)(e_acsl_49),
+            (__mpz_struct const *)(e_acsl_50));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)y);
+    mpz_init((__mpz_struct *)(e_acsl_54));
+    mpz_sub((__mpz_struct *)(e_acsl_54),(__mpz_struct const *)(e_acsl_52),
+            (__mpz_struct const *)(e_acsl_53));
+    mpz_init((__mpz_struct *)(e_acsl_55));
+    mpz_add((__mpz_struct *)(e_acsl_55),(__mpz_struct const *)(e_acsl_51),
+            (__mpz_struct const *)(e_acsl_54));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)10);
+    mpz_init((__mpz_struct *)(e_acsl_57));
+    mpz_neg((__mpz_struct *)(e_acsl_57),(__mpz_struct const *)(e_acsl_56));
+    e_acsl_58 = mpz_cmp((__mpz_struct const *)(e_acsl_55),
+                        (__mpz_struct const *)(e_acsl_57));
+    if (e_acsl_58 != 0) {
       e_acsl_fail((char *)"(((x*2+(3+y))-4)+(x-y) == -10)");
-    } mpz_clear((__mpz_struct *)(e_acsl_cst_43));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_44));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_45));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_46));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_47));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_48));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_49));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_50));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_51));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_52));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_53));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_54));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_55));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_56));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_57));
+    } mpz_clear((__mpz_struct *)(e_acsl_43));
+    mpz_clear((__mpz_struct *)(e_acsl_44));
+    mpz_clear((__mpz_struct *)(e_acsl_45));
+    mpz_clear((__mpz_struct *)(e_acsl_46));
+    mpz_clear((__mpz_struct *)(e_acsl_47));
+    mpz_clear((__mpz_struct *)(e_acsl_48));
+    mpz_clear((__mpz_struct *)(e_acsl_49));
+    mpz_clear((__mpz_struct *)(e_acsl_50));
+    mpz_clear((__mpz_struct *)(e_acsl_51));
+    mpz_clear((__mpz_struct *)(e_acsl_52));
+    mpz_clear((__mpz_struct *)(e_acsl_53));
+    mpz_clear((__mpz_struct *)(e_acsl_54));
+    mpz_clear((__mpz_struct *)(e_acsl_55));
+    mpz_clear((__mpz_struct *)(e_acsl_56));
+    mpz_clear((__mpz_struct *)(e_acsl_57));
   }
   
   /*@ assert (0≡1) ≡ !(0≡0); */ ;
-  { mpz_t e_acsl_cst_59; mpz_t e_acsl_cst_60; int e_acsl_cst_61;
-    mpz_t e_acsl_cst_62; mpz_t e_acsl_cst_63; int e_acsl_cst_64;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_59),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_60),(long)1);
-    e_acsl_cst_61 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_59),
-                            (__mpz_struct const *)(e_acsl_cst_60));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_62),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_63),(long)0);
-    e_acsl_cst_64 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_62),
-                            (__mpz_struct const *)(e_acsl_cst_63));
-    if ((e_acsl_cst_61 == 0) != ! (e_acsl_cst_64 == 0)) {
+  { mpz_t e_acsl_59; mpz_t e_acsl_60; int e_acsl_61; mpz_t e_acsl_62;
+    mpz_t e_acsl_63; int e_acsl_64;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_60),(long)1);
+    e_acsl_61 = mpz_cmp((__mpz_struct const *)(e_acsl_59),
+                        (__mpz_struct const *)(e_acsl_60));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_62),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_63),(long)0);
+    e_acsl_64 = mpz_cmp((__mpz_struct const *)(e_acsl_62),
+                        (__mpz_struct const *)(e_acsl_63));
+    if ((e_acsl_61 == 0) != ! (e_acsl_64 == 0)) {
       e_acsl_fail((char *)"((0==1) == !(0==0))");
-    } mpz_clear((__mpz_struct *)(e_acsl_cst_59));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_60));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_62));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_63));
+    } mpz_clear((__mpz_struct *)(e_acsl_59));
+    mpz_clear((__mpz_struct *)(e_acsl_60));
+    mpz_clear((__mpz_struct *)(e_acsl_62));
+    mpz_clear((__mpz_struct *)(e_acsl_63));
   }
   
   /*@ assert (0≤-1) ≡ (0>0); */ ;
-  { mpz_t e_acsl_cst_65; mpz_t e_acsl_cst_66; mpz_t e_acsl_cst_67;
-    int e_acsl_cst_68; mpz_t e_acsl_cst_69; mpz_t e_acsl_cst_70;
-    int e_acsl_cst_71;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_65),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_66),(long)1);
-    mpz_init((__mpz_struct *)(e_acsl_cst_67));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_67),
-            (__mpz_struct const *)(e_acsl_cst_66));
-    e_acsl_cst_68 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_65),
-                            (__mpz_struct const *)(e_acsl_cst_67));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_69),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_70),(long)0);
-    e_acsl_cst_71 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_69),
-                            (__mpz_struct const *)(e_acsl_cst_70));
-    if ((e_acsl_cst_68 <= 0) != (e_acsl_cst_71 > 0)) {
+  { mpz_t e_acsl_65; mpz_t e_acsl_66; mpz_t e_acsl_67; int e_acsl_68;
+    mpz_t e_acsl_69; mpz_t e_acsl_70; int e_acsl_71;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_66),(long)1);
+    mpz_init((__mpz_struct *)(e_acsl_67));
+    mpz_neg((__mpz_struct *)(e_acsl_67),(__mpz_struct const *)(e_acsl_66));
+    e_acsl_68 = mpz_cmp((__mpz_struct const *)(e_acsl_65),
+                        (__mpz_struct const *)(e_acsl_67));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_70),(long)0);
+    e_acsl_71 = mpz_cmp((__mpz_struct const *)(e_acsl_69),
+                        (__mpz_struct const *)(e_acsl_70));
+    if ((e_acsl_68 <= 0) != (e_acsl_71 > 0)) {
       e_acsl_fail((char *)"((0<=-1) == (0>0))");
-    } mpz_clear((__mpz_struct *)(e_acsl_cst_65));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_66));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_67));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_69));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_70));
+    } mpz_clear((__mpz_struct *)(e_acsl_65));
+    mpz_clear((__mpz_struct *)(e_acsl_66));
+    mpz_clear((__mpz_struct *)(e_acsl_67));
+    mpz_clear((__mpz_struct *)(e_acsl_69));
+    mpz_clear((__mpz_struct *)(e_acsl_70));
   }
   
   /*@ assert (0≥-1) ≡ (0≤0); */ ;
-  { mpz_t e_acsl_cst_72; mpz_t e_acsl_cst_73; mpz_t e_acsl_cst_74;
-    int e_acsl_cst_75; mpz_t e_acsl_cst_76; mpz_t e_acsl_cst_77;
-    int e_acsl_cst_78;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_72),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_73),(long)1);
-    mpz_init((__mpz_struct *)(e_acsl_cst_74));
-    mpz_neg((__mpz_struct *)(e_acsl_cst_74),
-            (__mpz_struct const *)(e_acsl_cst_73));
-    e_acsl_cst_75 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_72),
-                            (__mpz_struct const *)(e_acsl_cst_74));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_76),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_77),(long)0);
-    e_acsl_cst_78 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_76),
-                            (__mpz_struct const *)(e_acsl_cst_77));
-    if ((e_acsl_cst_75 >= 0) != (e_acsl_cst_78 <= 0)) {
+  { mpz_t e_acsl_72; mpz_t e_acsl_73; mpz_t e_acsl_74; int e_acsl_75;
+    mpz_t e_acsl_76; mpz_t e_acsl_77; int e_acsl_78;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_72),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_73),(long)1);
+    mpz_init((__mpz_struct *)(e_acsl_74));
+    mpz_neg((__mpz_struct *)(e_acsl_74),(__mpz_struct const *)(e_acsl_73));
+    e_acsl_75 = mpz_cmp((__mpz_struct const *)(e_acsl_72),
+                        (__mpz_struct const *)(e_acsl_74));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_76),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_77),(long)0);
+    e_acsl_78 = mpz_cmp((__mpz_struct const *)(e_acsl_76),
+                        (__mpz_struct const *)(e_acsl_77));
+    if ((e_acsl_75 >= 0) != (e_acsl_78 <= 0)) {
       e_acsl_fail((char *)"((0>=-1) == (0<=0))");
-    } mpz_clear((__mpz_struct *)(e_acsl_cst_72));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_73));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_74));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_76));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_77));
+    } mpz_clear((__mpz_struct *)(e_acsl_72));
+    mpz_clear((__mpz_struct *)(e_acsl_73));
+    mpz_clear((__mpz_struct *)(e_acsl_74));
+    mpz_clear((__mpz_struct *)(e_acsl_76));
+    mpz_clear((__mpz_struct *)(e_acsl_77));
   }
   
   /*@ assert (0≢1) ≡ !(0≢0); */ ;
-  { mpz_t e_acsl_cst_79; mpz_t e_acsl_cst_80; int e_acsl_cst_81;
-    mpz_t e_acsl_cst_82; mpz_t e_acsl_cst_83; int e_acsl_cst_84;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_79),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_80),(long)1);
-    e_acsl_cst_81 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_79),
-                            (__mpz_struct const *)(e_acsl_cst_80));
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_82),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_83),(long)0);
-    e_acsl_cst_84 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_82),
-                            (__mpz_struct const *)(e_acsl_cst_83));
-    if ((e_acsl_cst_81 != 0) != ! (e_acsl_cst_84 != 0)) {
+  { mpz_t e_acsl_79; mpz_t e_acsl_80; int e_acsl_81; mpz_t e_acsl_82;
+    mpz_t e_acsl_83; int e_acsl_84;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_79),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_80),(long)1);
+    e_acsl_81 = mpz_cmp((__mpz_struct const *)(e_acsl_79),
+                        (__mpz_struct const *)(e_acsl_80));
+    mpz_init_set_si((__mpz_struct *)(e_acsl_82),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_83),(long)0);
+    e_acsl_84 = mpz_cmp((__mpz_struct const *)(e_acsl_82),
+                        (__mpz_struct const *)(e_acsl_83));
+    if ((e_acsl_81 != 0) != ! (e_acsl_84 != 0)) {
       e_acsl_fail((char *)"((0!=1) == !(0!=0))");
-    } mpz_clear((__mpz_struct *)(e_acsl_cst_79));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_80));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_82));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_83));
+    } mpz_clear((__mpz_struct *)(e_acsl_79));
+    mpz_clear((__mpz_struct *)(e_acsl_80));
+    mpz_clear((__mpz_struct *)(e_acsl_82));
+    mpz_clear((__mpz_struct *)(e_acsl_83));
   }
   
   return;
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 3bad225e6b5e7a9bd3e1cf16c844d9ac6af2056c..35578bea611fdf3596f303e499da1ea828e346a4 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
@@ -29,7 +29,7 @@ PROJECT_FILE.i:105:[value] Function exit: postcondition got status invalid
 [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.
+        Called from PROJECT_FILE.i:134.
 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.
@@ -56,7 +56,7 @@ PROJECT_FILE.i:138:[value] Assertion got status valid.
 [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:143.
+        Called from PROJECT_FILE.i:142.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:143.
@@ -84,7 +84,7 @@ PROJECT_FILE.i:153:[value] Assertion got status valid.
 [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:158.
+        Called from PROJECT_FILE.i:157.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:158.
@@ -110,7 +110,7 @@ PROJECT_FILE.i:161:[value] Assertion got status valid.
 [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:166.
+        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.
@@ -136,7 +136,7 @@ PROJECT_FILE.i:169:[value] Assertion got status valid.
 [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:174.
+        Called from PROJECT_FILE.i:173.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:174.
@@ -162,7 +162,7 @@ PROJECT_FILE.i:177:[value] Assertion got status valid.
 [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:182.
+        Called from PROJECT_FILE.i:181.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:182.
@@ -214,7 +214,7 @@ PROJECT_FILE.i:193:[value] Assertion got status valid.
 [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:198.
+        Called from PROJECT_FILE.i:197.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:198.
@@ -288,25 +288,25 @@ void main(void)
   /*@ assert y > x; */ ;
   if (y <= x) { e_acsl_fail((char *)"(y > x)"); }
   /*@ assert x ≤ 0; */ ;
-  { mpz_t e_acsl_cst_1; mpz_t e_acsl_cst_2; int e_acsl_cst_3;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long)x);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_2),(long)0);
-    e_acsl_cst_3 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_1),
-                           (__mpz_struct const *)(e_acsl_cst_2));
-    if (e_acsl_cst_3 > 0) { e_acsl_fail((char *)"(x <= 0)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_1));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_2));
+  { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+    e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
+                       (__mpz_struct const *)(e_acsl_2));
+    if (e_acsl_3 > 0) { e_acsl_fail((char *)"(x <= 0)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_1));
+    mpz_clear((__mpz_struct *)(e_acsl_2));
   }
   
   /*@ assert y ≥ 1; */ ;
-  { mpz_t e_acsl_cst_4; mpz_t e_acsl_cst_5; int e_acsl_cst_6;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_4),(long)y);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long)1);
-    e_acsl_cst_6 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_4),
-                           (__mpz_struct const *)(e_acsl_cst_5));
-    if (e_acsl_cst_6 < 0) { e_acsl_fail((char *)"(y >= 1)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_4));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_5));
+  { mpz_t e_acsl_4; mpz_t e_acsl_5; int e_acsl_6;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)y);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
+    e_acsl_6 = mpz_cmp((__mpz_struct const *)(e_acsl_4),
+                       (__mpz_struct const *)(e_acsl_5));
+    if (e_acsl_6 < 0) { e_acsl_fail((char *)"(y >= 1)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_4));
+    mpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
   s = (char *)"toto";
@@ -315,69 +315,69 @@ void main(void)
   /*@ assert "toto" ≢ "titi"; */ ;
   if ("toto" == "titi") { e_acsl_fail((char *)"(\"toto\" != \"titi\")"); }
   /*@ assert 5 < 18; */ ;
-  { mpz_t e_acsl_cst_7; mpz_t e_acsl_cst_8; int e_acsl_cst_9;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_7),(long)5);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_8),(long)18);
-    e_acsl_cst_9 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_7),
-                           (__mpz_struct const *)(e_acsl_cst_8));
-    if (e_acsl_cst_9 >= 0) { e_acsl_fail((char *)"(5 < 18)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_7));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_8));
+  { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)5);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)18);
+    e_acsl_9 = mpz_cmp((__mpz_struct const *)(e_acsl_7),
+                       (__mpz_struct const *)(e_acsl_8));
+    if (e_acsl_9 >= 0) { e_acsl_fail((char *)"(5 < 18)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_7));
+    mpz_clear((__mpz_struct *)(e_acsl_8));
   }
   
   /*@ assert 32 > 3; */ ;
-  { mpz_t e_acsl_cst_10; mpz_t e_acsl_cst_11; int e_acsl_cst_12;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_10),(long)32);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_11),(long)3);
-    e_acsl_cst_12 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_10),
-                            (__mpz_struct const *)(e_acsl_cst_11));
-    if (e_acsl_cst_12 <= 0) { e_acsl_fail((char *)"(32 > 3)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_10));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_11));
+  { mpz_t e_acsl_10; mpz_t e_acsl_11; int e_acsl_12;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)32);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)3);
+    e_acsl_12 = mpz_cmp((__mpz_struct const *)(e_acsl_10),
+                        (__mpz_struct const *)(e_acsl_11));
+    if (e_acsl_12 <= 0) { e_acsl_fail((char *)"(32 > 3)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_10));
+    mpz_clear((__mpz_struct *)(e_acsl_11));
   }
   
   /*@ assert 12 ≤ 13; */ ;
-  { mpz_t e_acsl_cst_13; mpz_t e_acsl_cst_14; int e_acsl_cst_15;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_13),(long)12);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_14),(long)13);
-    e_acsl_cst_15 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_13),
-                            (__mpz_struct const *)(e_acsl_cst_14));
-    if (e_acsl_cst_15 > 0) { e_acsl_fail((char *)"(12 <= 13)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_13));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_14));
+  { mpz_t e_acsl_13; mpz_t e_acsl_14; int e_acsl_15;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_13),(long)12);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)13);
+    e_acsl_15 = mpz_cmp((__mpz_struct const *)(e_acsl_13),
+                        (__mpz_struct const *)(e_acsl_14));
+    if (e_acsl_15 > 0) { e_acsl_fail((char *)"(12 <= 13)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_13));
+    mpz_clear((__mpz_struct *)(e_acsl_14));
   }
   
   /*@ assert 123 ≥ 12; */ ;
-  { mpz_t e_acsl_cst_16; mpz_t e_acsl_cst_17; int e_acsl_cst_18;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_16),(long)123);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_17),(long)12);
-    e_acsl_cst_18 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_16),
-                            (__mpz_struct const *)(e_acsl_cst_17));
-    if (e_acsl_cst_18 < 0) { e_acsl_fail((char *)"(123 >= 12)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_16));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_17));
+  { mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)123);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_17),(long)12);
+    e_acsl_18 = mpz_cmp((__mpz_struct const *)(e_acsl_16),
+                        (__mpz_struct const *)(e_acsl_17));
+    if (e_acsl_18 < 0) { e_acsl_fail((char *)"(123 >= 12)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_16));
+    mpz_clear((__mpz_struct *)(e_acsl_17));
   }
   
   /*@ assert 0xff ≡ 0xff; */ ;
-  { mpz_t e_acsl_cst_19; mpz_t e_acsl_cst_20; int e_acsl_cst_21;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_19),(long)0xff);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_20),(long)0xff);
-    e_acsl_cst_21 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_19),
-                            (__mpz_struct const *)(e_acsl_cst_20));
-    if (e_acsl_cst_21 != 0) { e_acsl_fail((char *)"(0xff == 0xff)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_19));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_20));
+  { mpz_t e_acsl_19; mpz_t e_acsl_20; int e_acsl_21;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)0xff);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)0xff);
+    e_acsl_21 = mpz_cmp((__mpz_struct const *)(e_acsl_19),
+                        (__mpz_struct const *)(e_acsl_20));
+    if (e_acsl_21 != 0) { e_acsl_fail((char *)"(0xff == 0xff)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_19));
+    mpz_clear((__mpz_struct *)(e_acsl_20));
   }
   
   /*@ assert 1 ≢ 2; */ ;
-  { mpz_t e_acsl_cst_22; mpz_t e_acsl_cst_23; int e_acsl_cst_24;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_22),(long)1);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_23),(long)2);
-    e_acsl_cst_24 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_22),
-                            (__mpz_struct const *)(e_acsl_cst_23));
-    if (e_acsl_cst_24 == 0) { e_acsl_fail((char *)"(1 != 2)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_22));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_23));
+  { mpz_t e_acsl_22; mpz_t e_acsl_23; int e_acsl_24;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)1);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)2);
+    e_acsl_24 = mpz_cmp((__mpz_struct const *)(e_acsl_22),
+                        (__mpz_struct const *)(e_acsl_23));
+    if (e_acsl_24 == 0) { e_acsl_fail((char *)"(1 != 2)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_22));
+    mpz_clear((__mpz_struct *)(e_acsl_23));
   }
   
   return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 8ac46cc1f64e0ce14c771ea582f1f45bc265b226..fabb402fb4b283fcdb5fa26ab2f2c7008f97efdc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -613,314 +613,287 @@ void main(void)
   x = -3;
   y = 2;
   /*@ assert -3 ≡ x; */ ;
-  { mpz_t e_acsl_cst_1; mpz_t e_acsl_cst_2; mpz_t e_acsl_cst_3;
-    int e_acsl_cst_4;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long)3);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_2));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_2),
-               (__mpz_struct const *)(e_acsl_cst_1));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_3),(long)x);
-    e_acsl_cst_4 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_2),
-                              (__mpz_struct const *)(e_acsl_cst_3));
-    if (e_acsl_cst_4 != 0) { e_acsl_fail((char *)"(-3 == x)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_1));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_2));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_3));
+  { mpz_t e_acsl_1; mpz_t e_acsl_2; mpz_t e_acsl_3; int e_acsl_4;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)3);
+    __gmpz_init((__mpz_struct *)(e_acsl_2));
+    __gmpz_neg((__mpz_struct *)(e_acsl_2),(__mpz_struct const *)(e_acsl_1));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_3),(long)x);
+    e_acsl_4 = __gmpz_cmp((__mpz_struct const *)(e_acsl_2),
+                          (__mpz_struct const *)(e_acsl_3));
+    if (e_acsl_4 != 0) { e_acsl_fail((char *)"(-3 == x)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_1));
+    __gmpz_clear((__mpz_struct *)(e_acsl_2));
+    __gmpz_clear((__mpz_struct *)(e_acsl_3));
   }
   
   /*@ assert x ≡ -3; */ ;
-  { mpz_t e_acsl_cst_5; mpz_t e_acsl_cst_6; mpz_t e_acsl_cst_7;
-    int e_acsl_cst_8;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_6),(long)3);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_7));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_7),
-               (__mpz_struct const *)(e_acsl_cst_6));
-    e_acsl_cst_8 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_5),
-                              (__mpz_struct const *)(e_acsl_cst_7));
-    if (e_acsl_cst_8 != 0) { e_acsl_fail((char *)"(x == -3)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_5));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_6));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_7));
+  { mpz_t e_acsl_5; mpz_t e_acsl_6; mpz_t e_acsl_7; int e_acsl_8;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_6),(long)3);
+    __gmpz_init((__mpz_struct *)(e_acsl_7));
+    __gmpz_neg((__mpz_struct *)(e_acsl_7),(__mpz_struct const *)(e_acsl_6));
+    e_acsl_8 = __gmpz_cmp((__mpz_struct const *)(e_acsl_5),
+                          (__mpz_struct const *)(e_acsl_7));
+    if (e_acsl_8 != 0) { e_acsl_fail((char *)"(x == -3)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_5));
+    __gmpz_clear((__mpz_struct *)(e_acsl_6));
+    __gmpz_clear((__mpz_struct *)(e_acsl_7));
   }
   
   /*@ assert 0 ≢ ~0; */ ;
-  { mpz_t e_acsl_cst_9; mpz_t e_acsl_cst_10; mpz_t e_acsl_cst_11;
-    int e_acsl_cst_12;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_9),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_10),(long)0);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_11));
-    __gmpz_com(e_acsl_cst_11,(__mpz_struct const *)(e_acsl_cst_10));
-    e_acsl_cst_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_9),
-                               (__mpz_struct const *)(e_acsl_cst_11));
-    if (e_acsl_cst_12 == 0) { e_acsl_fail((char *)"(0 != ~0)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_9));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_10));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_11));
+  { mpz_t e_acsl_9; mpz_t e_acsl_10; mpz_t e_acsl_11; int e_acsl_12;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)0);
+    __gmpz_init((__mpz_struct *)(e_acsl_11));
+    __gmpz_com(e_acsl_11,(__mpz_struct const *)(e_acsl_10));
+    e_acsl_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_9),
+                           (__mpz_struct const *)(e_acsl_11));
+    if (e_acsl_12 == 0) { e_acsl_fail((char *)"(0 != ~0)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_9));
+    __gmpz_clear((__mpz_struct *)(e_acsl_10));
+    __gmpz_clear((__mpz_struct *)(e_acsl_11));
   }
   
   /*@ assert x+1 ≡ -2; */ ;
-  { mpz_t e_acsl_cst_13; mpz_t e_acsl_cst_14; mpz_t e_acsl_cst_15;
-    mpz_t e_acsl_cst_16; mpz_t e_acsl_cst_17; int e_acsl_cst_18;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_13),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_14),(long)1);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_15));
-    __gmpz_add((__mpz_struct *)(e_acsl_cst_15),
-               (__mpz_struct const *)(e_acsl_cst_13),
-               (__mpz_struct const *)(e_acsl_cst_14));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_16),(long)2);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_17));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_17),
-               (__mpz_struct const *)(e_acsl_cst_16));
-    e_acsl_cst_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_15),
-                               (__mpz_struct const *)(e_acsl_cst_17));
-    if (e_acsl_cst_18 != 0) { e_acsl_fail((char *)"(x+1 == -2)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_13));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_14));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_15));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_16));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_17));
+  { mpz_t e_acsl_13; mpz_t e_acsl_14; mpz_t e_acsl_15; mpz_t e_acsl_16;
+    mpz_t e_acsl_17; int e_acsl_18;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_13),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)1);
+    __gmpz_init((__mpz_struct *)(e_acsl_15));
+    __gmpz_add((__mpz_struct *)(e_acsl_15),(__mpz_struct const *)(e_acsl_13),
+               (__mpz_struct const *)(e_acsl_14));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)2);
+    __gmpz_init((__mpz_struct *)(e_acsl_17));
+    __gmpz_neg((__mpz_struct *)(e_acsl_17),(__mpz_struct const *)(e_acsl_16));
+    e_acsl_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_15),
+                           (__mpz_struct const *)(e_acsl_17));
+    if (e_acsl_18 != 0) { e_acsl_fail((char *)"(x+1 == -2)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_13));
+    __gmpz_clear((__mpz_struct *)(e_acsl_14));
+    __gmpz_clear((__mpz_struct *)(e_acsl_15));
+    __gmpz_clear((__mpz_struct *)(e_acsl_16));
+    __gmpz_clear((__mpz_struct *)(e_acsl_17));
   }
   
   /*@ assert x-1 ≡ -4; */ ;
-  { mpz_t e_acsl_cst_19; mpz_t e_acsl_cst_20; mpz_t e_acsl_cst_21;
-    mpz_t e_acsl_cst_22; mpz_t e_acsl_cst_23; int e_acsl_cst_24;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_19),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_20),(long)1);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_21));
-    __gmpz_sub((__mpz_struct *)(e_acsl_cst_21),
-               (__mpz_struct const *)(e_acsl_cst_19),
-               (__mpz_struct const *)(e_acsl_cst_20));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_22),(long)4);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_23));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_23),
-               (__mpz_struct const *)(e_acsl_cst_22));
-    e_acsl_cst_24 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_21),
-                               (__mpz_struct const *)(e_acsl_cst_23));
-    if (e_acsl_cst_24 != 0) { e_acsl_fail((char *)"(x-1 == -4)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_19));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_20));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_21));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_22));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_23));
+  { mpz_t e_acsl_19; mpz_t e_acsl_20; mpz_t e_acsl_21; mpz_t e_acsl_22;
+    mpz_t e_acsl_23; int e_acsl_24;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)1);
+    __gmpz_init((__mpz_struct *)(e_acsl_21));
+    __gmpz_sub((__mpz_struct *)(e_acsl_21),(__mpz_struct const *)(e_acsl_19),
+               (__mpz_struct const *)(e_acsl_20));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)4);
+    __gmpz_init((__mpz_struct *)(e_acsl_23));
+    __gmpz_neg((__mpz_struct *)(e_acsl_23),(__mpz_struct const *)(e_acsl_22));
+    e_acsl_24 = __gmpz_cmp((__mpz_struct const *)(e_acsl_21),
+                           (__mpz_struct const *)(e_acsl_23));
+    if (e_acsl_24 != 0) { e_acsl_fail((char *)"(x-1 == -4)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_19));
+    __gmpz_clear((__mpz_struct *)(e_acsl_20));
+    __gmpz_clear((__mpz_struct *)(e_acsl_21));
+    __gmpz_clear((__mpz_struct *)(e_acsl_22));
+    __gmpz_clear((__mpz_struct *)(e_acsl_23));
   }
   
   /*@ assert x*3 ≡ -9; */ ;
-  { mpz_t e_acsl_cst_25; mpz_t e_acsl_cst_26; mpz_t e_acsl_cst_27;
-    mpz_t e_acsl_cst_28; mpz_t e_acsl_cst_29; int e_acsl_cst_30;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_25),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_26),(long)3);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_27));
-    __gmpz_mul((__mpz_struct *)(e_acsl_cst_27),
-               (__mpz_struct const *)(e_acsl_cst_25),
-               (__mpz_struct const *)(e_acsl_cst_26));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_28),(long)9);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_29));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_29),
-               (__mpz_struct const *)(e_acsl_cst_28));
-    e_acsl_cst_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_27),
-                               (__mpz_struct const *)(e_acsl_cst_29));
-    if (e_acsl_cst_30 != 0) { e_acsl_fail((char *)"(x*3 == -9)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_25));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_26));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_27));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_28));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_29));
+  { mpz_t e_acsl_25; mpz_t e_acsl_26; mpz_t e_acsl_27; mpz_t e_acsl_28;
+    mpz_t e_acsl_29; int e_acsl_30;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_25),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)3);
+    __gmpz_init((__mpz_struct *)(e_acsl_27));
+    __gmpz_mul((__mpz_struct *)(e_acsl_27),(__mpz_struct const *)(e_acsl_25),
+               (__mpz_struct const *)(e_acsl_26));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_28),(long)9);
+    __gmpz_init((__mpz_struct *)(e_acsl_29));
+    __gmpz_neg((__mpz_struct *)(e_acsl_29),(__mpz_struct const *)(e_acsl_28));
+    e_acsl_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_27),
+                           (__mpz_struct const *)(e_acsl_29));
+    if (e_acsl_30 != 0) { e_acsl_fail((char *)"(x*3 == -9)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_25));
+    __gmpz_clear((__mpz_struct *)(e_acsl_26));
+    __gmpz_clear((__mpz_struct *)(e_acsl_27));
+    __gmpz_clear((__mpz_struct *)(e_acsl_28));
+    __gmpz_clear((__mpz_struct *)(e_acsl_29));
   }
   
   /*@ assert x/3 ≡ -1; */ ;
-  { mpz_t e_acsl_cst_31; mpz_t e_acsl_cst_32; mpz_t e_acsl_cst_33;
-    mpz_t e_acsl_cst_34; mpz_t e_acsl_cst_35; int e_acsl_cst_36;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_31),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_32),(long)3);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_33));
-    __gmpz_cdiv_q((__mpz_struct *)(e_acsl_cst_33),
-                  (__mpz_struct const *)(e_acsl_cst_31),
-                  (__mpz_struct const *)(e_acsl_cst_32));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_34),(long)1);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_35));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_35),
-               (__mpz_struct const *)(e_acsl_cst_34));
-    e_acsl_cst_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_33),
-                               (__mpz_struct const *)(e_acsl_cst_35));
-    if (e_acsl_cst_36 != 0) { e_acsl_fail((char *)"(x/3 == -1)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_31));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_32));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_33));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_34));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_35));
+  { mpz_t e_acsl_31; mpz_t e_acsl_32; mpz_t e_acsl_33; mpz_t e_acsl_34;
+    mpz_t e_acsl_35; int e_acsl_36;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_32),(long)3);
+    __gmpz_init((__mpz_struct *)(e_acsl_33));
+    __gmpz_cdiv_q((__mpz_struct *)(e_acsl_33),
+                  (__mpz_struct const *)(e_acsl_31),
+                  (__mpz_struct const *)(e_acsl_32));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)1);
+    __gmpz_init((__mpz_struct *)(e_acsl_35));
+    __gmpz_neg((__mpz_struct *)(e_acsl_35),(__mpz_struct const *)(e_acsl_34));
+    e_acsl_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_33),
+                           (__mpz_struct const *)(e_acsl_35));
+    if (e_acsl_36 != 0) { e_acsl_fail((char *)"(x/3 == -1)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_31));
+    __gmpz_clear((__mpz_struct *)(e_acsl_32));
+    __gmpz_clear((__mpz_struct *)(e_acsl_33));
+    __gmpz_clear((__mpz_struct *)(e_acsl_34));
+    __gmpz_clear((__mpz_struct *)(e_acsl_35));
   }
   
   /*@ assert x%2 ≡ -1; */ ;
-  { mpz_t e_acsl_cst_37; mpz_t e_acsl_cst_38; mpz_t e_acsl_cst_39;
-    mpz_t e_acsl_cst_40; mpz_t e_acsl_cst_41; int e_acsl_cst_42;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_37),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_38),(long)2);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_39));
-    __gmpz_mod((__mpz_struct *)(e_acsl_cst_39),
-               (__mpz_struct const *)(e_acsl_cst_37),
-               (__mpz_struct const *)(e_acsl_cst_38));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_40),(long)1);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_41));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_41),
-               (__mpz_struct const *)(e_acsl_cst_40));
-    e_acsl_cst_42 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_39),
-                               (__mpz_struct const *)(e_acsl_cst_41));
-    if (e_acsl_cst_42 != 0) { e_acsl_fail((char *)"(x%2 == -1)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_37));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_38));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_39));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_40));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_41));
+  { mpz_t e_acsl_37; mpz_t e_acsl_38; mpz_t e_acsl_39; mpz_t e_acsl_40;
+    mpz_t e_acsl_41; int e_acsl_42;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)2);
+    __gmpz_init((__mpz_struct *)(e_acsl_39));
+    __gmpz_mod((__mpz_struct *)(e_acsl_39),(__mpz_struct const *)(e_acsl_37),
+               (__mpz_struct const *)(e_acsl_38));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)1);
+    __gmpz_init((__mpz_struct *)(e_acsl_41));
+    __gmpz_neg((__mpz_struct *)(e_acsl_41),(__mpz_struct const *)(e_acsl_40));
+    e_acsl_42 = __gmpz_cmp((__mpz_struct const *)(e_acsl_39),
+                           (__mpz_struct const *)(e_acsl_41));
+    if (e_acsl_42 != 0) { e_acsl_fail((char *)"(x%2 == -1)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_37));
+    __gmpz_clear((__mpz_struct *)(e_acsl_38));
+    __gmpz_clear((__mpz_struct *)(e_acsl_39));
+    __gmpz_clear((__mpz_struct *)(e_acsl_40));
+    __gmpz_clear((__mpz_struct *)(e_acsl_41));
   }
   
   /*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */ ;
-  { mpz_t e_acsl_cst_43; mpz_t e_acsl_cst_44; mpz_t e_acsl_cst_45;
-    mpz_t e_acsl_cst_46; mpz_t e_acsl_cst_47; mpz_t e_acsl_cst_48;
-    mpz_t e_acsl_cst_49; mpz_t e_acsl_cst_50; mpz_t e_acsl_cst_51;
-    mpz_t e_acsl_cst_52; mpz_t e_acsl_cst_53; mpz_t e_acsl_cst_54;
-    mpz_t e_acsl_cst_55; mpz_t e_acsl_cst_56; mpz_t e_acsl_cst_57;
-    int e_acsl_cst_58;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_43),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_44),(long)2);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_45));
-    __gmpz_mul((__mpz_struct *)(e_acsl_cst_45),
-               (__mpz_struct const *)(e_acsl_cst_43),
-               (__mpz_struct const *)(e_acsl_cst_44));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_46),(long)3);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_47),(long)y);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_48));
-    __gmpz_add((__mpz_struct *)(e_acsl_cst_48),
-               (__mpz_struct const *)(e_acsl_cst_46),
-               (__mpz_struct const *)(e_acsl_cst_47));
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_49));
-    __gmpz_add((__mpz_struct *)(e_acsl_cst_49),
-               (__mpz_struct const *)(e_acsl_cst_45),
-               (__mpz_struct const *)(e_acsl_cst_48));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_50),(long)4);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_51));
-    __gmpz_sub((__mpz_struct *)(e_acsl_cst_51),
-               (__mpz_struct const *)(e_acsl_cst_49),
-               (__mpz_struct const *)(e_acsl_cst_50));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_52),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_53),(long)y);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_54));
-    __gmpz_sub((__mpz_struct *)(e_acsl_cst_54),
-               (__mpz_struct const *)(e_acsl_cst_52),
-               (__mpz_struct const *)(e_acsl_cst_53));
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_55));
-    __gmpz_add((__mpz_struct *)(e_acsl_cst_55),
-               (__mpz_struct const *)(e_acsl_cst_51),
-               (__mpz_struct const *)(e_acsl_cst_54));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_56),(long)10);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_57));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_57),
-               (__mpz_struct const *)(e_acsl_cst_56));
-    e_acsl_cst_58 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_55),
-                               (__mpz_struct const *)(e_acsl_cst_57));
-    if (e_acsl_cst_58 != 0) {
+  { mpz_t e_acsl_43; mpz_t e_acsl_44; mpz_t e_acsl_45; mpz_t e_acsl_46;
+    mpz_t e_acsl_47; mpz_t e_acsl_48; mpz_t e_acsl_49; mpz_t e_acsl_50;
+    mpz_t e_acsl_51; mpz_t e_acsl_52; mpz_t e_acsl_53; mpz_t e_acsl_54;
+    mpz_t e_acsl_55; mpz_t e_acsl_56; mpz_t e_acsl_57; int e_acsl_58;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_43),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_44),(long)2);
+    __gmpz_init((__mpz_struct *)(e_acsl_45));
+    __gmpz_mul((__mpz_struct *)(e_acsl_45),(__mpz_struct const *)(e_acsl_43),
+               (__mpz_struct const *)(e_acsl_44));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_46),(long)3);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_47),(long)y);
+    __gmpz_init((__mpz_struct *)(e_acsl_48));
+    __gmpz_add((__mpz_struct *)(e_acsl_48),(__mpz_struct const *)(e_acsl_46),
+               (__mpz_struct const *)(e_acsl_47));
+    __gmpz_init((__mpz_struct *)(e_acsl_49));
+    __gmpz_add((__mpz_struct *)(e_acsl_49),(__mpz_struct const *)(e_acsl_45),
+               (__mpz_struct const *)(e_acsl_48));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)4);
+    __gmpz_init((__mpz_struct *)(e_acsl_51));
+    __gmpz_sub((__mpz_struct *)(e_acsl_51),(__mpz_struct const *)(e_acsl_49),
+               (__mpz_struct const *)(e_acsl_50));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_53),(long)y);
+    __gmpz_init((__mpz_struct *)(e_acsl_54));
+    __gmpz_sub((__mpz_struct *)(e_acsl_54),(__mpz_struct const *)(e_acsl_52),
+               (__mpz_struct const *)(e_acsl_53));
+    __gmpz_init((__mpz_struct *)(e_acsl_55));
+    __gmpz_add((__mpz_struct *)(e_acsl_55),(__mpz_struct const *)(e_acsl_51),
+               (__mpz_struct const *)(e_acsl_54));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_56),(long)10);
+    __gmpz_init((__mpz_struct *)(e_acsl_57));
+    __gmpz_neg((__mpz_struct *)(e_acsl_57),(__mpz_struct const *)(e_acsl_56));
+    e_acsl_58 = __gmpz_cmp((__mpz_struct const *)(e_acsl_55),
+                           (__mpz_struct const *)(e_acsl_57));
+    if (e_acsl_58 != 0) {
       e_acsl_fail((char *)"(((x*2+(3+y))-4)+(x-y) == -10)");
-    } __gmpz_clear((__mpz_struct *)(e_acsl_cst_43));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_44));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_45));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_46));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_47));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_48));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_49));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_50));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_51));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_52));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_53));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_54));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_55));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_56));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_57));
+    } __gmpz_clear((__mpz_struct *)(e_acsl_43));
+    __gmpz_clear((__mpz_struct *)(e_acsl_44));
+    __gmpz_clear((__mpz_struct *)(e_acsl_45));
+    __gmpz_clear((__mpz_struct *)(e_acsl_46));
+    __gmpz_clear((__mpz_struct *)(e_acsl_47));
+    __gmpz_clear((__mpz_struct *)(e_acsl_48));
+    __gmpz_clear((__mpz_struct *)(e_acsl_49));
+    __gmpz_clear((__mpz_struct *)(e_acsl_50));
+    __gmpz_clear((__mpz_struct *)(e_acsl_51));
+    __gmpz_clear((__mpz_struct *)(e_acsl_52));
+    __gmpz_clear((__mpz_struct *)(e_acsl_53));
+    __gmpz_clear((__mpz_struct *)(e_acsl_54));
+    __gmpz_clear((__mpz_struct *)(e_acsl_55));
+    __gmpz_clear((__mpz_struct *)(e_acsl_56));
+    __gmpz_clear((__mpz_struct *)(e_acsl_57));
   }
   
   /*@ assert (0≡1) ≡ !(0≡0); */ ;
-  { mpz_t e_acsl_cst_59; mpz_t e_acsl_cst_60; int e_acsl_cst_61;
-    mpz_t e_acsl_cst_62; mpz_t e_acsl_cst_63; int e_acsl_cst_64;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_59),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_60),(long)1);
-    e_acsl_cst_61 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_59),
-                               (__mpz_struct const *)(e_acsl_cst_60));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_62),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_63),(long)0);
-    e_acsl_cst_64 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_62),
-                               (__mpz_struct const *)(e_acsl_cst_63));
-    if ((e_acsl_cst_61 == 0) != ! (e_acsl_cst_64 == 0)) {
+  { mpz_t e_acsl_59; mpz_t e_acsl_60; int e_acsl_61; mpz_t e_acsl_62;
+    mpz_t e_acsl_63; int e_acsl_64;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_60),(long)1);
+    e_acsl_61 = __gmpz_cmp((__mpz_struct const *)(e_acsl_59),
+                           (__mpz_struct const *)(e_acsl_60));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_62),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_63),(long)0);
+    e_acsl_64 = __gmpz_cmp((__mpz_struct const *)(e_acsl_62),
+                           (__mpz_struct const *)(e_acsl_63));
+    if ((e_acsl_61 == 0) != ! (e_acsl_64 == 0)) {
       e_acsl_fail((char *)"((0==1) == !(0==0))");
-    } __gmpz_clear((__mpz_struct *)(e_acsl_cst_59));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_60));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_62));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_63));
+    } __gmpz_clear((__mpz_struct *)(e_acsl_59));
+    __gmpz_clear((__mpz_struct *)(e_acsl_60));
+    __gmpz_clear((__mpz_struct *)(e_acsl_62));
+    __gmpz_clear((__mpz_struct *)(e_acsl_63));
   }
   
   /*@ assert (0≤-1) ≡ (0>0); */ ;
-  { mpz_t e_acsl_cst_65; mpz_t e_acsl_cst_66; mpz_t e_acsl_cst_67;
-    int e_acsl_cst_68; mpz_t e_acsl_cst_69; mpz_t e_acsl_cst_70;
-    int e_acsl_cst_71;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_65),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_66),(long)1);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_67));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_67),
-               (__mpz_struct const *)(e_acsl_cst_66));
-    e_acsl_cst_68 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_65),
-                               (__mpz_struct const *)(e_acsl_cst_67));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_69),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_70),(long)0);
-    e_acsl_cst_71 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_69),
-                               (__mpz_struct const *)(e_acsl_cst_70));
-    if ((e_acsl_cst_68 <= 0) != (e_acsl_cst_71 > 0)) {
+  { mpz_t e_acsl_65; mpz_t e_acsl_66; mpz_t e_acsl_67; int e_acsl_68;
+    mpz_t e_acsl_69; mpz_t e_acsl_70; int e_acsl_71;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_65),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_66),(long)1);
+    __gmpz_init((__mpz_struct *)(e_acsl_67));
+    __gmpz_neg((__mpz_struct *)(e_acsl_67),(__mpz_struct const *)(e_acsl_66));
+    e_acsl_68 = __gmpz_cmp((__mpz_struct const *)(e_acsl_65),
+                           (__mpz_struct const *)(e_acsl_67));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_69),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_70),(long)0);
+    e_acsl_71 = __gmpz_cmp((__mpz_struct const *)(e_acsl_69),
+                           (__mpz_struct const *)(e_acsl_70));
+    if ((e_acsl_68 <= 0) != (e_acsl_71 > 0)) {
       e_acsl_fail((char *)"((0<=-1) == (0>0))");
-    } __gmpz_clear((__mpz_struct *)(e_acsl_cst_65));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_66));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_67));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_69));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_70));
+    } __gmpz_clear((__mpz_struct *)(e_acsl_65));
+    __gmpz_clear((__mpz_struct *)(e_acsl_66));
+    __gmpz_clear((__mpz_struct *)(e_acsl_67));
+    __gmpz_clear((__mpz_struct *)(e_acsl_69));
+    __gmpz_clear((__mpz_struct *)(e_acsl_70));
   }
   
   /*@ assert (0≥-1) ≡ (0≤0); */ ;
-  { mpz_t e_acsl_cst_72; mpz_t e_acsl_cst_73; mpz_t e_acsl_cst_74;
-    int e_acsl_cst_75; mpz_t e_acsl_cst_76; mpz_t e_acsl_cst_77;
-    int e_acsl_cst_78;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_72),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_73),(long)1);
-    __gmpz_init((__mpz_struct *)(e_acsl_cst_74));
-    __gmpz_neg((__mpz_struct *)(e_acsl_cst_74),
-               (__mpz_struct const *)(e_acsl_cst_73));
-    e_acsl_cst_75 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_72),
-                               (__mpz_struct const *)(e_acsl_cst_74));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_76),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_77),(long)0);
-    e_acsl_cst_78 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_76),
-                               (__mpz_struct const *)(e_acsl_cst_77));
-    if ((e_acsl_cst_75 >= 0) != (e_acsl_cst_78 <= 0)) {
+  { mpz_t e_acsl_72; mpz_t e_acsl_73; mpz_t e_acsl_74; int e_acsl_75;
+    mpz_t e_acsl_76; mpz_t e_acsl_77; int e_acsl_78;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_72),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_73),(long)1);
+    __gmpz_init((__mpz_struct *)(e_acsl_74));
+    __gmpz_neg((__mpz_struct *)(e_acsl_74),(__mpz_struct const *)(e_acsl_73));
+    e_acsl_75 = __gmpz_cmp((__mpz_struct const *)(e_acsl_72),
+                           (__mpz_struct const *)(e_acsl_74));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_76),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_77),(long)0);
+    e_acsl_78 = __gmpz_cmp((__mpz_struct const *)(e_acsl_76),
+                           (__mpz_struct const *)(e_acsl_77));
+    if ((e_acsl_75 >= 0) != (e_acsl_78 <= 0)) {
       e_acsl_fail((char *)"((0>=-1) == (0<=0))");
-    } __gmpz_clear((__mpz_struct *)(e_acsl_cst_72));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_73));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_74));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_76));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_77));
+    } __gmpz_clear((__mpz_struct *)(e_acsl_72));
+    __gmpz_clear((__mpz_struct *)(e_acsl_73));
+    __gmpz_clear((__mpz_struct *)(e_acsl_74));
+    __gmpz_clear((__mpz_struct *)(e_acsl_76));
+    __gmpz_clear((__mpz_struct *)(e_acsl_77));
   }
   
   /*@ assert (0≢1) ≡ !(0≢0); */ ;
-  { mpz_t e_acsl_cst_79; mpz_t e_acsl_cst_80; int e_acsl_cst_81;
-    mpz_t e_acsl_cst_82; mpz_t e_acsl_cst_83; int e_acsl_cst_84;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_79),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_80),(long)1);
-    e_acsl_cst_81 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_79),
-                               (__mpz_struct const *)(e_acsl_cst_80));
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_82),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_83),(long)0);
-    e_acsl_cst_84 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_82),
-                               (__mpz_struct const *)(e_acsl_cst_83));
-    if ((e_acsl_cst_81 != 0) != ! (e_acsl_cst_84 != 0)) {
+  { mpz_t e_acsl_79; mpz_t e_acsl_80; int e_acsl_81; mpz_t e_acsl_82;
+    mpz_t e_acsl_83; int e_acsl_84;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_79),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_80),(long)1);
+    e_acsl_81 = __gmpz_cmp((__mpz_struct const *)(e_acsl_79),
+                           (__mpz_struct const *)(e_acsl_80));
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_82),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_83),(long)0);
+    e_acsl_84 = __gmpz_cmp((__mpz_struct const *)(e_acsl_82),
+                           (__mpz_struct const *)(e_acsl_83));
+    if ((e_acsl_81 != 0) != ! (e_acsl_84 != 0)) {
       e_acsl_fail((char *)"((0!=1) == !(0!=0))");
-    } __gmpz_clear((__mpz_struct *)(e_acsl_cst_79));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_80));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_82));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_83));
+    } __gmpz_clear((__mpz_struct *)(e_acsl_79));
+    __gmpz_clear((__mpz_struct *)(e_acsl_80));
+    __gmpz_clear((__mpz_struct *)(e_acsl_82));
+    __gmpz_clear((__mpz_struct *)(e_acsl_83));
   }
   
   return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 1acb31f7a326fa6cf5088be460d26ae429050647..5e05e161569236cfc5f6b03b349e8e15e60047aa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -574,25 +574,25 @@ void main(void)
   /*@ assert y > x; */ ;
   if (y <= x) { e_acsl_fail((char *)"(y > x)"); }
   /*@ assert x ≤ 0; */ ;
-  { mpz_t e_acsl_cst_1; mpz_t e_acsl_cst_2; int e_acsl_cst_3;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long)x);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_2),(long)0);
-    e_acsl_cst_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_1),
-                              (__mpz_struct const *)(e_acsl_cst_2));
-    if (e_acsl_cst_3 > 0) { e_acsl_fail((char *)"(x <= 0)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_1));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_2));
+  { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+    e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+                          (__mpz_struct const *)(e_acsl_2));
+    if (e_acsl_3 > 0) { e_acsl_fail((char *)"(x <= 0)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_1));
+    __gmpz_clear((__mpz_struct *)(e_acsl_2));
   }
   
   /*@ assert y ≥ 1; */ ;
-  { mpz_t e_acsl_cst_4; mpz_t e_acsl_cst_5; int e_acsl_cst_6;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_4),(long)y);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long)1);
-    e_acsl_cst_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_4),
-                              (__mpz_struct const *)(e_acsl_cst_5));
-    if (e_acsl_cst_6 < 0) { e_acsl_fail((char *)"(y >= 1)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_4));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_5));
+  { mpz_t e_acsl_4; mpz_t e_acsl_5; int e_acsl_6;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)y);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
+    e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
+                          (__mpz_struct const *)(e_acsl_5));
+    if (e_acsl_6 < 0) { e_acsl_fail((char *)"(y >= 1)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_4));
+    __gmpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
   s = (char *)"toto";
@@ -601,69 +601,69 @@ void main(void)
   /*@ assert "toto" ≢ "titi"; */ ;
   if ("toto" == "titi") { e_acsl_fail((char *)"(\"toto\" != \"titi\")"); }
   /*@ assert 5 < 18; */ ;
-  { mpz_t e_acsl_cst_7; mpz_t e_acsl_cst_8; int e_acsl_cst_9;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_7),(long)5);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_8),(long)18);
-    e_acsl_cst_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_7),
-                              (__mpz_struct const *)(e_acsl_cst_8));
-    if (e_acsl_cst_9 >= 0) { e_acsl_fail((char *)"(5 < 18)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_7));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_8));
+  { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)5);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)18);
+    e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
+                          (__mpz_struct const *)(e_acsl_8));
+    if (e_acsl_9 >= 0) { e_acsl_fail((char *)"(5 < 18)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_7));
+    __gmpz_clear((__mpz_struct *)(e_acsl_8));
   }
   
   /*@ assert 32 > 3; */ ;
-  { mpz_t e_acsl_cst_10; mpz_t e_acsl_cst_11; int e_acsl_cst_12;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_10),(long)32);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_11),(long)3);
-    e_acsl_cst_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_10),
-                               (__mpz_struct const *)(e_acsl_cst_11));
-    if (e_acsl_cst_12 <= 0) { e_acsl_fail((char *)"(32 > 3)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_10));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_11));
+  { mpz_t e_acsl_10; mpz_t e_acsl_11; int e_acsl_12;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)32);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)3);
+    e_acsl_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_10),
+                           (__mpz_struct const *)(e_acsl_11));
+    if (e_acsl_12 <= 0) { e_acsl_fail((char *)"(32 > 3)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_10));
+    __gmpz_clear((__mpz_struct *)(e_acsl_11));
   }
   
   /*@ assert 12 ≤ 13; */ ;
-  { mpz_t e_acsl_cst_13; mpz_t e_acsl_cst_14; int e_acsl_cst_15;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_13),(long)12);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_14),(long)13);
-    e_acsl_cst_15 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_13),
-                               (__mpz_struct const *)(e_acsl_cst_14));
-    if (e_acsl_cst_15 > 0) { e_acsl_fail((char *)"(12 <= 13)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_13));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_14));
+  { mpz_t e_acsl_13; mpz_t e_acsl_14; int e_acsl_15;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_13),(long)12);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_14),(long)13);
+    e_acsl_15 = __gmpz_cmp((__mpz_struct const *)(e_acsl_13),
+                           (__mpz_struct const *)(e_acsl_14));
+    if (e_acsl_15 > 0) { e_acsl_fail((char *)"(12 <= 13)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_13));
+    __gmpz_clear((__mpz_struct *)(e_acsl_14));
   }
   
   /*@ assert 123 ≥ 12; */ ;
-  { mpz_t e_acsl_cst_16; mpz_t e_acsl_cst_17; int e_acsl_cst_18;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_16),(long)123);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_17),(long)12);
-    e_acsl_cst_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_16),
-                               (__mpz_struct const *)(e_acsl_cst_17));
-    if (e_acsl_cst_18 < 0) { e_acsl_fail((char *)"(123 >= 12)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_16));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_17));
+  { mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)123);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_17),(long)12);
+    e_acsl_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_16),
+                           (__mpz_struct const *)(e_acsl_17));
+    if (e_acsl_18 < 0) { e_acsl_fail((char *)"(123 >= 12)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_16));
+    __gmpz_clear((__mpz_struct *)(e_acsl_17));
   }
   
   /*@ assert 0xff ≡ 0xff; */ ;
-  { mpz_t e_acsl_cst_19; mpz_t e_acsl_cst_20; int e_acsl_cst_21;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_19),(long)0xff);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_20),(long)0xff);
-    e_acsl_cst_21 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_19),
-                               (__mpz_struct const *)(e_acsl_cst_20));
-    if (e_acsl_cst_21 != 0) { e_acsl_fail((char *)"(0xff == 0xff)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_19));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_20));
+  { mpz_t e_acsl_19; mpz_t e_acsl_20; int e_acsl_21;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_19),(long)0xff);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)0xff);
+    e_acsl_21 = __gmpz_cmp((__mpz_struct const *)(e_acsl_19),
+                           (__mpz_struct const *)(e_acsl_20));
+    if (e_acsl_21 != 0) { e_acsl_fail((char *)"(0xff == 0xff)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_19));
+    __gmpz_clear((__mpz_struct *)(e_acsl_20));
   }
   
   /*@ assert 1 ≢ 2; */ ;
-  { mpz_t e_acsl_cst_22; mpz_t e_acsl_cst_23; int e_acsl_cst_24;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_22),(long)1);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_23),(long)2);
-    e_acsl_cst_24 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_22),
-                               (__mpz_struct const *)(e_acsl_cst_23));
-    if (e_acsl_cst_24 == 0) { e_acsl_fail((char *)"(1 != 2)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_22));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_23));
+  { mpz_t e_acsl_22; mpz_t e_acsl_23; int e_acsl_24;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)1);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_23),(long)2);
+    e_acsl_24 = __gmpz_cmp((__mpz_struct const *)(e_acsl_22),
+                           (__mpz_struct const *)(e_acsl_23));
+    if (e_acsl_24 == 0) { e_acsl_fail((char *)"(1 != 2)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_22));
+    __gmpz_clear((__mpz_struct *)(e_acsl_23));
   }
   
   return;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 5321f7ffd6e55feb3e3616f0d48e85a9385c090d..fc364dd68c01220b4fa69d33acf4e667c9699237 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -569,39 +569,37 @@ void e_acsl_fail(char *msg)
 void main(void)
 {
   /*@ assert 0 ≡ 0; */ ;
-  { mpz_t e_acsl_cst_1; mpz_t e_acsl_cst_2; int e_acsl_cst_3;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_2),(long)0);
-    e_acsl_cst_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_1),
-                              (__mpz_struct const *)(e_acsl_cst_2));
-    if (e_acsl_cst_3 != 0) { e_acsl_fail((char *)"(0 == 0)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_1));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_2));
+  { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+    e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+                          (__mpz_struct const *)(e_acsl_2));
+    if (e_acsl_3 != 0) { e_acsl_fail((char *)"(0 == 0)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_1));
+    __gmpz_clear((__mpz_struct *)(e_acsl_2));
   }
   
   /*@ assert 0 ≢ 1; */ ;
-  { mpz_t e_acsl_cst_4; mpz_t e_acsl_cst_5; int e_acsl_cst_6;
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_4),(long)0);
-    __gmpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long)1);
-    e_acsl_cst_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_4),
-                              (__mpz_struct const *)(e_acsl_cst_5));
-    if (e_acsl_cst_6 == 0) { e_acsl_fail((char *)"(0 != 1)"); }
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_4));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_5));
+  { mpz_t e_acsl_4; mpz_t e_acsl_5; int e_acsl_6;
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)0);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
+    e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
+                          (__mpz_struct const *)(e_acsl_5));
+    if (e_acsl_6 == 0) { e_acsl_fail((char *)"(0 != 1)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_4));
+    __gmpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
   /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
-  { mpz_t e_acsl_cst_7; mpz_t e_acsl_cst_8; int e_acsl_cst_9;
-    __gmpz_init_set_str((__mpz_struct *)(e_acsl_cst_7),"1152921504606846975",
-                        10);
-    __gmpz_init_set_str((__mpz_struct *)(e_acsl_cst_8),"1152921504606846975",
-                        10);
-    e_acsl_cst_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_cst_7),
-                              (__mpz_struct const *)(e_acsl_cst_8));
-    if (e_acsl_cst_9 != 0) {
+  { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
+    __gmpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
+    __gmpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
+    e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
+                          (__mpz_struct const *)(e_acsl_8));
+    if (e_acsl_9 != 0) {
       e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
-    } __gmpz_clear((__mpz_struct *)(e_acsl_cst_7));
-    __gmpz_clear((__mpz_struct *)(e_acsl_cst_8));
+    } __gmpz_clear((__mpz_struct *)(e_acsl_7));
+    __gmpz_clear((__mpz_struct *)(e_acsl_8));
   }
   
   return;
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 93a5b40aae97251247c3f35ef672c6271d9179ca..c8382f6512eb221a7d3bc7dd5a23e6a98c20421e 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
@@ -27,7 +27,7 @@ PROJECT_FILE.i:105:[value] Function exit: postcondition got status invalid
 [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.
+        Called from PROJECT_FILE.i:123.
 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.
@@ -54,7 +54,7 @@ PROJECT_FILE.i:127:[value] Assertion got status valid.
 [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:132.
+        Called from PROJECT_FILE.i:131.
 [value] Done for function mpz_clear
 [value] computing for function mpz_clear <- main.
         Called from PROJECT_FILE.i:132.
@@ -149,37 +149,37 @@ void e_acsl_fail(char *msg)
 void main(void)
 {
   /*@ assert 0 ≡ 0; */ ;
-  { mpz_t e_acsl_cst_1; mpz_t e_acsl_cst_2; int e_acsl_cst_3;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_1),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_2),(long)0);
-    e_acsl_cst_3 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_1),
-                           (__mpz_struct const *)(e_acsl_cst_2));
-    if (e_acsl_cst_3 != 0) { e_acsl_fail((char *)"(0 == 0)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_1));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_2));
+  { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+    e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
+                       (__mpz_struct const *)(e_acsl_2));
+    if (e_acsl_3 != 0) { e_acsl_fail((char *)"(0 == 0)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_1));
+    mpz_clear((__mpz_struct *)(e_acsl_2));
   }
   
   /*@ assert 0 ≢ 1; */ ;
-  { mpz_t e_acsl_cst_4; mpz_t e_acsl_cst_5; int e_acsl_cst_6;
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_4),(long)0);
-    mpz_init_set_si((__mpz_struct *)(e_acsl_cst_5),(long)1);
-    e_acsl_cst_6 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_4),
-                           (__mpz_struct const *)(e_acsl_cst_5));
-    if (e_acsl_cst_6 == 0) { e_acsl_fail((char *)"(0 != 1)"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_4));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_5));
+  { mpz_t e_acsl_4; mpz_t e_acsl_5; int e_acsl_6;
+    mpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)0);
+    mpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
+    e_acsl_6 = mpz_cmp((__mpz_struct const *)(e_acsl_4),
+                       (__mpz_struct const *)(e_acsl_5));
+    if (e_acsl_6 == 0) { e_acsl_fail((char *)"(0 != 1)"); }
+    mpz_clear((__mpz_struct *)(e_acsl_4));
+    mpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
   /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
-  { mpz_t e_acsl_cst_7; mpz_t e_acsl_cst_8; int e_acsl_cst_9;
-    mpz_init_set_str((__mpz_struct *)(e_acsl_cst_7),"1152921504606846975",10);
-    mpz_init_set_str((__mpz_struct *)(e_acsl_cst_8),"1152921504606846975",10);
-    e_acsl_cst_9 = mpz_cmp((__mpz_struct const *)(e_acsl_cst_7),
-                           (__mpz_struct const *)(e_acsl_cst_8));
-    if (e_acsl_cst_9 != 0) {
+  { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
+    mpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
+    mpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
+    e_acsl_9 = mpz_cmp((__mpz_struct const *)(e_acsl_7),
+                       (__mpz_struct const *)(e_acsl_8));
+    if (e_acsl_9 != 0) {
       e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
-    } mpz_clear((__mpz_struct *)(e_acsl_cst_7));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_8));
+    } mpz_clear((__mpz_struct *)(e_acsl_7));
+    mpz_clear((__mpz_struct *)(e_acsl_8));
   }
   
   return;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index dcfb10833614b0b0848606ccdcd15cc430e03021..931c9fba94b3e89d65c892632aa0dfcdab009f37 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -46,10 +46,10 @@ let e_acsl_header () = GText (Read_header.text ())
 (* Build a C conditional doing a runtime assertion check. *)
 let mk_if e p =
   let loc = p.loc in
-  let no_uni = Parameters.Unicode.get () in
+  let unicode = Parameters.Unicode.get () in
   Parameters.Unicode.off ();
   let msg = Pretty_utils.sfprintf "%a@?" Cil.d_predicate_named p in
-  Parameters.Unicode.set no_uni;
+  Parameters.Unicode.set unicode;
   let s = mk_call ~loc "e_acsl_fail" [ mkString loc msg ] in
   mkStmt ~valid_sid:true (If(e, mkBlock [ s ], mkBlock [], loc))
 
@@ -131,7 +131,7 @@ end = struct
 	~generated:true
 	false (* is a global? *)
 	false (* is a formal? *)
-	("e_acsl_cst_" ^ string_of_int !var_cpt)
+	("e_acsl_" ^ string_of_int !var_cpt)
 	ty
     in
     let e = new_lval v in