diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
index 39946e50b149fcb452fdd858f0dfba24b28ac6c7..302d9979e34c50d5264fadd0797160f534b2f272 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
@@ -294,6 +294,27 @@ extern void __gmpq_div(mpq_t q1, const mpq_t q2, const mpq_t q3)
 /* Bitwise operators */
 /*********************/
 
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_and(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_ior(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_xor(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
 /*@ requires \valid(z1);
   @ requires \valid_read(z2);
   @ assigns *z1 \from *z2;