diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index 847f278af6728c9aee5713fd548f6c60a63ea745..d9aa69130314a0b55e45d6ef8ef003280fc3b5a7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -935,15 +935,11 @@ extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2;
@@ -953,7 +949,6 @@ extern void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -964,7 +959,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -975,7 +969,6 @@ extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -986,7 +979,6 @@ extern void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -997,7 +989,6 @@ extern void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -1007,7 +998,6 @@ extern void __gmpz_tdiv_r(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index ea501c71f67291f52c370c74a7a7126317145bc0..32676167d9a7c9094b77c39649e36d367758b0a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -94,10 +94,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index b45c3443e0b6fb13c09812f2d3ddb33c84af29cc..9f974a7586c0a2a9955c11586a9a4d4ddecafcd3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -361,16 +361,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index ed07f2aae5261205d0a3c46a5b23a516f9cd8fc3..617fbeb9b06dfb0dda37ee84afacef7cf17e466d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -205,14 +205,10 @@ extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index a8422130298d4cab345995f5bc9569dcd73db782..8d7271e6ad96eaf37173dda5ce89f20cbdc9ba51 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -428,15 +428,11 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index 1349b58541fa9d9824ca4063b13ee7af6e9e0cb5..09ac08bf81e2ff594c6541ed4d7dc9256050d8cb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -767,16 +767,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 56383fbba5dd62973c3b29b7091288fde7a8340e..4e94ab1b73f1e0bb6d1801bf0f93df62a870faf7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -101,10 +101,7 @@ extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index 67addf88e851fcf6e34ec14a1b55987b992d2b02..08cb2156355a04f32a511324c96bff1cb699c32b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -898,10 +898,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index b4b7eb9185460bcaaa743ef7188fabba4cde9b18..ab7a257340cf33622c6375a8c439918b48843c68 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -121,10 +121,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index 850904b8e6252dad7c14b88bdb310147a05e292d..0696b151a6ec3ccdf35384e059ad6ec1d9159685 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -850,10 +850,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index 8ec0a1bd963fa41674b8367793e214fb747f1e97..6cbaee68747b4d94d2a6e28efe406c954d4f7987 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -614,7 +614,6 @@ extern void __gmpz_init(__mpz_struct * /*[1]*/ z);
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
/*@ requires \valid(z_orig);
requires \valid(z);
- allocates \nothing;
assigns *z;
assigns *z \from *z_orig;
@@ -628,16 +627,12 @@ extern void __gmpz_set(__mpz_struct * /*[1]*/ z,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -646,7 +641,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index 1dd6cf46a5cfe06eca18aa2fab3b79533540c003..03dd5637ee0e49824cb1819066841014ba9d5dc3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -177,10 +177,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index 87fa944cb5736153d70e2ce4aeda0fdfacb804bd..6da46777f1c37aeffef4024123938adbfd8ae00e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -62,10 +62,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index 18fb24716643bf15b33f1134dbb6366cc7f8e761..72cc668a4e80a8ff45aa018864364b0a95956c1e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -86,10 +86,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index 108825f9d75885b8c71cb782c6c86afaa68e420e..e55d6bf42bee0b3d37092d642a041af938e928ef 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -488,16 +488,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -508,7 +504,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -519,7 +514,6 @@ extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -530,7 +524,6 @@ extern void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -539,7 +532,6 @@ extern void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index a24ca4fadd810d28410a296dfa7eba48501628aa..9e297890cd4548e4fb580799050954bc95fffa05 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -694,7 +694,6 @@ extern void __gmpz_init(__mpz_struct * /*[1]*/ z);
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
/*@ requires \valid(z_orig);
requires \valid(z);
- allocates \nothing;
assigns *z;
assigns *z \from *z_orig;
@@ -708,16 +707,12 @@ extern void __gmpz_set(__mpz_struct * /*[1]*/ z,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -728,7 +723,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -739,7 +733,6 @@ extern void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -750,7 +743,6 @@ extern void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index 2407d0bb8af6a5b15b3f172aa309bafe312437d2..b393f8f389ec6d1b19f42b038a4666301f2b045f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -156,16 +156,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -174,7 +170,6 @@ extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index db802e14f78c6bfa1d277e1dabb8453089040e0f..ac837bb1d27ebfc2ff37c5fbc26e60b0b4f25cf0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -62,10 +62,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index be8d36c24c90a577a2f5f42f731cb84098f0e32e..ad0d833045564946de56289fcd192ef95727cb88 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -475,16 +475,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index 8be306ba07ce805d19e537a9b3df8e6684bd42ec..50bb0f56db16bd5f90a0daa4bcc32cbd17d0b0b9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -72,10 +72,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;