diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
new file mode 100644
index 0000000000000000000000000000000000000000..33386ccc44a15031dcc7a3ae9a75ab790a0eb195
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -0,0 +1,659 @@
+/* Generated by Frama-C */
+typedef unsigned long size_t;
+typedef unsigned long mp_limb_t;
+struct __anonstruct___mpz_struct_6 {
+ int _mp_alloc ;
+ int _mp_size ;
+ mp_limb_t *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_6 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+typedef mp_limb_t *mp_ptr;
+typedef mp_limb_t const *mp_srcptr;
+typedef long mp_size_t;
+struct __anonstruct___mpq_struct_7 {
+ __mpz_struct _mp_num ;
+ __mpz_struct _mp_den ;
+};
+typedef struct __anonstruct___mpq_struct_7 __mpq_struct;
+typedef __mpz_struct const *mpz_srcptr;
+typedef __mpz_struct *mpz_ptr;
+typedef __mpq_struct const *mpq_srcptr;
+typedef __mpq_struct *mpq_ptr;
+/* compiler builtin:
+ long __builtin_expect(long, long); */
+/*@ assigns \nothing; */
+extern int printf(char const * __restrict __format , ...);
+__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n) __attribute__((
+__pure__));
+/*@ ensures \valid(\old(x));
+ assigns *x; */
+extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
+ __mpz_struct const * /*[1]*/ z_orig);
+/*@ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from n; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
+__pure__));
+extern void __gmpz_set(mpz_ptr, mpz_srcptr);
+__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u);
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+extern void __gmpz_tdiv_q(mpz_ptr, mpz_srcptr, mpz_srcptr);
+__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
+__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
+extern void __gmpq_set(mpq_ptr, mpq_srcptr);
+__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize);
+__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n);
+extern mp_limb_t __gmpn_add_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size) __attribute__((__pure__));
+__inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
+ mp_size_t __gmp_n);
+extern int __gmpn_perfect_square_p(mp_srcptr, mp_size_t) __attribute__((
+__pure__));
+extern unsigned long __gmpn_popcount(mp_srcptr, mp_size_t) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize);
+__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n);
+extern mp_limb_t __gmpn_sub_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
+__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpz_set(__gmp_w,__gmp_u); }
+ if (__gmp_w->_mp_size >= 0) { __gmp_w->_mp_size = __gmp_w->_mp_size; }
+ else { __gmp_w->_mp_size = - __gmp_w->_mp_size; }
+ return;
+}
+
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (long)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= (mp_limb_t)(~ ((unsigned int)0))) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (long)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= ~ ((unsigned long)0)) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
+{
+ int __retres;
+ mp_size_t __gmp_n;
+ mp_ptr __gmp_p;
+ int tmp;
+ __gmp_n = (long)__gmp_z->_mp_size;
+ __gmp_p = __gmp_z->_mp_d;
+ if (__gmp_n == (mp_size_t)0) { tmp = 1; }
+ else {
+ if (__gmp_n == (mp_size_t)1) {
+ if (*(__gmp_p + 0) <= (mp_limb_t)((unsigned short)(~ 0))) { tmp = 1; }
+ else { tmp = 0; }
+ }
+ else { tmp = 0; }
+ }
+ __retres = tmp;
+ goto return_label;
+ return_label: /* internal */
+ return (__retres);
+}
+
+/*@ requires \valid(z);
+ assigns \nothing; */
+__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z)
+{
+ mp_ptr __gmp_p;
+ mp_size_t __gmp_n;
+ mp_limb_t __gmp_l;
+ mp_limb_t tmp;
+ __gmp_p = z->_mp_d;
+ __gmp_n = (long)z->_mp_size;
+ __gmp_l = *(__gmp_p + 0);
+ if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
+ else { tmp = (unsigned long)0; }
+ return (tmp);
+}
+
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n) __attribute__((
+__pure__));
+__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
+ mp_size_t __gmp_n)
+{
+ mp_limb_t __gmp_result;
+ long tmp_1;
+ int tmp_0;
+ __gmp_result = (unsigned long)0;
+ { /*undefined sequence*/
+ if (__gmp_n >= (mp_size_t)0) {
+ int tmp;
+ { /*undefined sequence*/
+ if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
+ else { tmp = - __gmp_z->_mp_size; }
+ ;
+ }
+ if (__gmp_n < (mp_size_t)tmp) { tmp_0 = 1; }
+ else { tmp_0 = 0; }
+ }
+ else { tmp_0 = 0; }
+ tmp_1 = __builtin_expect((long)(tmp_0 != 0),(long)1);
+ }
+ if (tmp_1) { __gmp_result = *(__gmp_z->_mp_d + __gmp_n); }
+ return (__gmp_result);
+}
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns *z1; */
+__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2)
+{
+ if (z1 != z2) { __gmpz_set(z1,z2); }
+ z1->_mp_size = - z1->_mp_size;
+ return;
+}
+
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
+__pure__));
+__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a)
+{
+ mp_size_t __gmp_asize;
+ int __gmp_result;
+ long tmp;
+ __gmp_asize = (long)__gmp_a->_mp_size;
+ __gmp_result = __gmp_asize >= (mp_size_t)0;
+ tmp = __builtin_expect((long)((__gmp_asize > (mp_size_t)0) != 0),(long)1);
+ if (tmp) {
+ __gmp_result = __gmpn_perfect_square_p((mp_limb_t const *)__gmp_a->_mp_d,
+ __gmp_asize);
+ }
+ return (__gmp_result);
+}
+
+__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
+__pure__));
+__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u)
+{
+ mp_size_t __gmp_usize;
+ unsigned long __gmp_result;
+ long tmp;
+ __gmp_usize = (long)__gmp_u->_mp_size;
+ if (__gmp_usize < (mp_size_t)0) { __gmp_result = ~ ((unsigned long)0); }
+ else { __gmp_result = (unsigned long)0; }
+ tmp = __builtin_expect((long)((__gmp_usize > (mp_size_t)0) != 0),(long)1);
+ if (tmp) {
+ __gmp_result = __gmpn_popcount((mp_limb_t const *)__gmp_u->_mp_d,
+ __gmp_usize);
+ }
+ return (__gmp_result);
+}
+
+__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ __gmpz_tdiv_q(__gmp_w,& __gmp_u->_mp_num,& __gmp_u->_mp_den);
+ return;
+}
+
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
+__pure__));
+__inline static size_t __gmpz_size(mpz_srcptr __gmp_z)
+{
+ size_t __retres;
+ int tmp;
+ if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
+ else { tmp = - __gmp_z->_mp_size; }
+ __retres = (unsigned long)tmp;
+ return (__retres);
+}
+
+__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
+ if (__gmp_w->_mp_num._mp_size >= 0) {
+ __gmp_w->_mp_num._mp_size = __gmp_w->_mp_num._mp_size;
+ }
+ else { __gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size; }
+ return;
+}
+
+__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
+{
+ if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
+ __gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size;
+ return;
+}
+
+__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; __gmp_i = __gmp_ysize;
+ if (__gmp_i != (mp_size_t)0) {
+ mp_limb_t tmp_1;
+ tmp_1 = __gmpn_add_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
+ if (tmp_1) {
+ while (1) {
+ mp_size_t tmp;
+ mp_limb_t tmp_0;
+ if (__gmp_i >= __gmp_xsize) {
+ __gmp_c = (unsigned long)1;
+ goto __gmp_done;
+ }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ { /*undefined sequence*/
+ tmp = __gmp_i;
+ __gmp_i += (mp_size_t)1;
+ tmp_0 = (__gmp_x + (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
+ *(__gmp_wp + tmp) = tmp_0;
+ }
+ if (! (tmp_0 == (mp_limb_t)0)) { break; }
+ }
+ }
+ }
+ if (__gmp_wp != __gmp_xp) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_xsize) {
+ *(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ } __gmp_c = (unsigned long)0; __gmp_done: ;
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_r;
+ __gmp_x = *(__gmp_src + 0); __gmp_r = __gmp_x + __gmp_n;
+ *(__gmp_dst + 0) = __gmp_r;
+ if (__gmp_r < __gmp_n) {
+ __gmp_c = (unsigned long)1;
+ __gmp_i = (long)1;
+ while (__gmp_i < __gmp_size) {
+ __gmp_x = *(__gmp_src + __gmp_i);
+ __gmp_r = __gmp_x + (mp_limb_t)1;
+ *(__gmp_dst + __gmp_i) = __gmp_r;
+ __gmp_i += (mp_size_t)1;
+ if (! (__gmp_r < (mp_limb_t)1)) {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_size) {
+ *(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ break;
+ }
+ }
+ }
+ else {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j_0; __gmp_j_0 = (long)1;
+ while (__gmp_j_0 < __gmp_size) {
+ *(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
+ __gmp_j_0 += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ }
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size) __attribute__((__pure__));
+__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
+ mp_size_t __gmp_size)
+{
+ int __gmp_result;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_y;
+ __gmp_result = 0; __gmp_i = __gmp_size;
+ while (1) {
+ __gmp_i -= (mp_size_t)1;
+ if (! (__gmp_i >= (mp_size_t)0)) { break; }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ __gmp_y = *(__gmp_yp + __gmp_i);
+ if (__gmp_x != __gmp_y) {
+ if (__gmp_x > __gmp_y) { __gmp_result = 1; }
+ else { __gmp_result = -1; }
+ break;
+ }
+ }
+ }
+
+ break;
+ }
+ return (__gmp_result);
+}
+
+__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
+ mp_size_t __gmp_xsize,
+ mp_srcptr __gmp_yp,
+ mp_size_t __gmp_ysize)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; __gmp_i = __gmp_ysize;
+ if (__gmp_i != (mp_size_t)0) {
+ mp_limb_t tmp_0;
+ tmp_0 = __gmpn_sub_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
+ if (tmp_0) {
+ while (1) {
+ mp_size_t tmp;
+ if (__gmp_i >= __gmp_xsize) {
+ __gmp_c = (unsigned long)1;
+ goto __gmp_done;
+ }
+ __gmp_x = *(__gmp_xp + __gmp_i);
+ { /*undefined sequence*/
+ tmp = __gmp_i;
+ __gmp_i += (mp_size_t)1;
+ *(__gmp_wp + tmp) = (__gmp_x - (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
+ }
+ if (! (__gmp_x == (mp_limb_t)0)) { break; }
+ }
+ }
+ }
+ if (__gmp_wp != __gmp_xp) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_xsize) {
+ *(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ } __gmp_c = (unsigned long)0; __gmp_done: ;
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
+ mp_size_t __gmp_size,
+ mp_limb_t __gmp_n)
+{
+ mp_limb_t __gmp_c;
+ while (1) {
+ { mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_r;
+ __gmp_x = *(__gmp_src + 0); __gmp_r = __gmp_x - __gmp_n;
+ *(__gmp_dst + 0) = __gmp_r;
+ if (__gmp_x < __gmp_n) {
+ __gmp_c = (unsigned long)1;
+ __gmp_i = (long)1;
+ while (__gmp_i < __gmp_size) {
+ __gmp_x = *(__gmp_src + __gmp_i);
+ __gmp_r = __gmp_x - (mp_limb_t)1;
+ *(__gmp_dst + __gmp_i) = __gmp_r;
+ __gmp_i += (mp_size_t)1;
+ if (! (__gmp_x < (mp_limb_t)1)) {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j; __gmp_j = __gmp_i;
+ while (__gmp_j < __gmp_size) {
+ *(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
+ __gmp_j += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ break;
+ }
+ }
+ }
+ else {
+ if (__gmp_src != __gmp_dst) {
+ while (1) {
+ { mp_size_t __gmp_j_0; __gmp_j_0 = (long)1;
+ while (__gmp_j_0 < __gmp_size) {
+ *(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
+ __gmp_j_0 += (mp_size_t)1;
+ }
+ }
+
+ break;
+ }
+ }
+ __gmp_c = (unsigned long)0;
+ }
+ }
+
+ break;
+ }
+ return (__gmp_c);
+}
+
+__inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
+ mp_size_t __gmp_n)
+{
+ mp_limb_t __gmp_ul;
+ mp_limb_t __gmp_cy;
+ __gmp_cy = (unsigned long)0;
+ while (1) {
+ { mp_srcptr tmp; mp_ptr tmp_0;
+ { /*undefined sequence*/ tmp = __gmp_up; __gmp_up ++; __gmp_ul = *tmp;
+ }
+ { /*undefined sequence*/
+ tmp_0 = __gmp_rp;
+ __gmp_rp ++;
+ *tmp_0 = - __gmp_ul - __gmp_cy;
+ } __gmp_cy |= (unsigned long)(__gmp_ul != (mp_limb_t)0);
+ }
+
+ __gmp_n -= (mp_size_t)1;
+ if (! (__gmp_n != (mp_size_t)0)) { break; }
+ }
+ return (__gmp_cy);
+}
+
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+void e_acsl_fail(char *msg)
+{
+ printf("%s\n",msg);
+ exit(1);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int x;
+ int e_acsl_4;
+ mpz_t e_acsl_11;
+ int e_acsl_14;
+ x = 0;
+ L: e_acsl_14 = x;
+ { mpz_t e_acsl_8; mpz_t e_acsl_9; mpz_t e_acsl_10;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_10));
+ __gmpz_add((__mpz_struct *)(e_acsl_10),(__mpz_struct const *)(e_acsl_8),
+ (__mpz_struct const *)(e_acsl_9));
+ __gmpz_init_set((__mpz_struct *)(e_acsl_11),
+ (__mpz_struct const *)(e_acsl_10));
+ __gmpz_clear((__mpz_struct *)(e_acsl_8));
+ __gmpz_clear((__mpz_struct *)(e_acsl_9));
+ __gmpz_clear((__mpz_struct *)(e_acsl_10));
+ }
+
+ e_acsl_4 = x;
+ /*@ assert x ≡ 0; */ ;
+ { 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));
+ }
+
+ x = 1;
+ x = 2;
+ /*@ assert \at(x,L) ≡ 0; */ ;
+ { mpz_t e_acsl_5; mpz_t e_acsl_6; int e_acsl_7;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)e_acsl_4);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_6),(long)0);
+ e_acsl_7 = __gmpz_cmp((__mpz_struct const *)(e_acsl_5),
+ (__mpz_struct const *)(e_acsl_6));
+ if (! (e_acsl_7 == 0)) { e_acsl_fail((char *)"(\\at(x,L) == 0)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_5));
+ __gmpz_clear((__mpz_struct *)(e_acsl_6));
+ }
+
+ /*@ assert \at(x+1,L) ≡ 1; */ ;
+ { mpz_t e_acsl_12; int e_acsl_13;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)1);
+ e_acsl_13 = __gmpz_cmp((__mpz_struct const *)(e_acsl_11),
+ (__mpz_struct const *)(e_acsl_12));
+ if (! (e_acsl_13 == 0)) { e_acsl_fail((char *)"(\\at(x+1,L) == 1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_12));
+ }
+
+ /*@ assert \at(x,L)+1 ≡ 1; */ ;
+ { 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_15),(long)e_acsl_14);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_17));
+ __gmpz_add((__mpz_struct *)(e_acsl_17),(__mpz_struct const *)(e_acsl_15),
+ (__mpz_struct const *)(e_acsl_16));
+ e_acsl_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_17),
+ (__mpz_struct const *)(e_acsl_16));
+ if (! (e_acsl_18 == 0)) { e_acsl_fail((char *)"(\\at(x,L)+1 == 1)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_15));
+ __gmpz_clear((__mpz_struct *)(e_acsl_16));
+ __gmpz_clear((__mpz_struct *)(e_acsl_17));
+ }
+
+ __retres = 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_11));
+ return (__retres);
+}
+
+