From f530c42462e96938ecd6163cc858bb18c7f47c35 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 28 May 2021 18:28:38 +0200
Subject: [PATCH] Update Why3 and refresh generated files.

---
 lib/add.c         |  6 +++---
 lib/addold.c      | 12 ++++++------
 lib/div.c         |  4 ++--
 lib/div.h         |  1 -
 lib/logical.c     | 14 +++++++-------
 lib/logical.h     |  1 -
 lib/logicalold.c  | 28 ++++++++++++++--------------
 lib/logicalold.h  |  1 -
 lib/logicalutil.c | 23 -----------------------
 lib/logicalutil.h | 15 ---------------
 lib/powm.h        |  1 -
 lib/sqrt.c        | 32 ++++++++++++++++----------------
 lib/sqrt.h        |  1 -
 lib/sub.c         |  6 +++---
 lib/subold.c      | 12 ++++++------
 lib/toom.c        | 20 ++++++++++----------
 lib/zadd.c        | 10 +++++-----
 lib/zdiv.c        | 10 +++++-----
 lib/zdiv2exp.h    |  1 -
 lib/zmul2exp.c    |  2 +-
 lib/zmul2exp.h    |  3 +--
 lib/zneg.c        | 26 ++++++++++++++++++++++++++
 lib/zneg.h        | 14 ++++++++++++++
 lib/zrealloc2.c   | 18 ++++++++++++++++++
 lib/zrealloc2.h   | 14 ++++++++++++++
 lib/zsub.c        | 10 +++++-----
 why3              |  2 +-
 27 files changed, 157 insertions(+), 130 deletions(-)
 delete mode 100644 lib/logicalutil.c
 delete mode 100644 lib/logicalutil.h
 create mode 100644 lib/zneg.c
 create mode 100644 lib/zneg.h
 create mode 100644 lib/zrealloc2.c
 create mode 100644 lib/zrealloc2.h

diff --git a/lib/add.c b/lib/add.c
index caa0289..71fdbeb 100644
--- a/lib/add.c
+++ b/lib/add.c
@@ -26,11 +26,11 @@ uint64_t wmpn_add_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
 uint64_t wmpn_add(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
                   int32_t sy) {
   uint64_t lx, c;
-  uint64_t o, res;
+  uint64_t result, res;
   int32_t i;
   lx = UINT64_C(0);
-  o = wmpn_add_n(r, x, y, sy);
-  c = o;
+  result = wmpn_add_n(r, x, y, sy);
+  c = result;
   i = sy;
   if (!(c == UINT64_C(0))) {
     while (i < sx) {
diff --git a/lib/addold.c b/lib/addold.c
index d5028eb..6d30ffb 100644
--- a/lib/addold.c
+++ b/lib/addold.c
@@ -26,11 +26,11 @@ uint64_t wmpn_add_n1(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
 uint64_t wmpn_add1(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
                    int32_t sy) {
   uint64_t lx, c;
-  uint64_t o, res;
+  uint64_t result, res;
   int32_t i;
   lx = UINT64_C(0);
-  o = wmpn_add_n1(r, x, y, sy);
-  c = o;
+  result = wmpn_add_n1(r, x, y, sy);
+  c = result;
   i = sy;
   if (!(c == UINT64_C(0))) {
     while (i < sx) {
@@ -76,11 +76,11 @@ uint64_t wmpn_add_n_in_place(uint64_t * x, uint64_t * y, int32_t sz) {
 
 uint64_t wmpn_add_in_place(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
   uint64_t lx, c;
-  uint64_t o, res;
+  uint64_t result, res;
   int32_t i;
   lx = UINT64_C(0);
-  o = wmpn_add_n_in_place(x, y, sy);
-  c = o;
+  result = wmpn_add_n_in_place(x, y, sy);
+  c = result;
   i = sy;
   if (!(c == UINT64_C(0))) {
     while (i < sx) {
diff --git a/lib/div.c b/lib/div.c
index b6a9b4c..644ae1a 100644
--- a/lib/div.c
+++ b/lib/div.c
@@ -47,7 +47,7 @@ uint64_t wmpn_divrem_1(uint64_t * q, uint64_t * x, int32_t sz, uint64_t y) {
   int32_t i;
   int32_t clz;
   uint64_t ry, v, l, h, qu, rem;
-  struct __lsld_ext_result struct_res;
+  struct __lsld64_result struct_res;
   struct __div2by1_inv_result struct_res1, struct_res2;
   uint64_t v1, qu1, rem1;
   msb = sz - 1;
@@ -60,7 +60,7 @@ uint64_t wmpn_divrem_1(uint64_t * q, uint64_t * x, int32_t sz, uint64_t y) {
     v = invert_limb(ry);
     while (i >= 0) {
       lx = x[i];
-      struct_res = lsld_ext(lx, (uint64_t)clz);
+      struct_res = lsld64(lx, (uint64_t)clz);
       l = struct_res.__field_0;
       h = struct_res.__field_1;
       struct_res1 = div2by1_inv(r + h, l, ry, v);
diff --git a/lib/div.h b/lib/div.h
index e189af3..b6b5756 100644
--- a/lib/div.h
+++ b/lib/div.h
@@ -6,7 +6,6 @@
 #include "utilold.h"
 #include "addold.h"
 #include "subold.h"
-#include "logicalutil.h"
 #include "logicalold.h"
 #include "mul.h"
 #include <stdint.h>
diff --git a/lib/logical.c b/lib/logical.c
index e2ac381..30f7d22 100644
--- a/lib/logical.c
+++ b/lib/logical.c
@@ -8,21 +8,21 @@ uint64_t wmpn_lshift(uint64_t * r, uint64_t * x, int32_t sz, uint64_t cnt) {
   uint64_t high, low;
   int32_t i;
   uint64_t l, retval, l1, h;
-  struct __lsld_ext_result struct_res, struct_res1;
+  struct __lsld64_result struct_res, struct_res1;
   msb = sz - 1;
   xp = x + msb;
   rp = r + msb;
   high = UINT64_C(0);
   low = *xp;
   i = msb;
-  struct_res = lsld_ext(low, cnt);
+  struct_res = lsld64(low, cnt);
   l = struct_res.__field_0;
   retval = struct_res.__field_1;
   high = l;
   while (i > 0) {
     xp = xp + -1;
     low = *xp;
-    struct_res1 = lsld_ext(low, cnt);
+    struct_res1 = lsld64(low, cnt);
     l1 = struct_res1.__field_0;
     h = struct_res1.__field_1;
     *rp = high + h;
@@ -41,17 +41,17 @@ uint64_t wmpn_rshift(uint64_t * r, uint64_t * x, int32_t sz, uint64_t cnt) {
   uint64_t * rp;
   uint64_t high;
   uint64_t retval, h;
-  struct __lsld_ext_result struct_res;
+  struct __lsld64_result struct_res;
   uint64_t low;
   int32_t i;
   uint64_t l, h1;
-  struct __lsld_ext_result struct_res1;
+  struct __lsld64_result struct_res1;
   tnc = UINT64_C(64) - cnt;
   msb = sz - 1;
   xp = x + 0;
   rp = r + 0;
   high = *xp;
-  struct_res = lsld_ext(high, tnc);
+  struct_res = lsld64(high, tnc);
   retval = struct_res.__field_0;
   h = struct_res.__field_1;
   low = h;
@@ -59,7 +59,7 @@ uint64_t wmpn_rshift(uint64_t * r, uint64_t * x, int32_t sz, uint64_t cnt) {
   while (i < msb) {
     xp = xp + 1;
     high = *xp;
-    struct_res1 = lsld_ext(high, tnc);
+    struct_res1 = lsld64(high, tnc);
     l = struct_res1.__field_0;
     h1 = struct_res1.__field_1;
     *rp = low + l;
diff --git a/lib/logical.h b/lib/logical.h
index 7e40360..27bbc0d 100644
--- a/lib/logical.h
+++ b/lib/logical.h
@@ -2,7 +2,6 @@
 
 #include "uint64gmp.h"
 #include "c.h"
-#include "logicalutil.h"
 #include "alias.h"
 #include <stdint.h>
 
diff --git a/lib/logicalold.c b/lib/logicalold.c
index 05f2abb..29698d6 100644
--- a/lib/logicalold.c
+++ b/lib/logicalold.c
@@ -8,21 +8,21 @@ uint64_t wmpn_lshift1(uint64_t * r, uint64_t * x, int32_t sz, uint64_t cnt) {
   uint64_t high, low;
   int32_t i;
   uint64_t l, retval, l1, h;
-  struct __lsld_ext_result struct_res, struct_res1;
+  struct __lsld64_result struct_res, struct_res1;
   msb = sz - 1;
   xp = x + msb;
   rp = r + msb;
   high = UINT64_C(0);
   low = *xp;
   i = msb;
-  struct_res = lsld_ext(low, cnt);
+  struct_res = lsld64(low, cnt);
   l = struct_res.__field_0;
   retval = struct_res.__field_1;
   high = l;
   while (i > 0) {
     xp = xp + -1;
     low = *xp;
-    struct_res1 = lsld_ext(low, cnt);
+    struct_res1 = lsld64(low, cnt);
     l1 = struct_res1.__field_0;
     h = struct_res1.__field_1;
     *rp = high + h;
@@ -41,17 +41,17 @@ uint64_t wmpn_rshift1(uint64_t * r, uint64_t * x, int32_t sz, uint64_t cnt) {
   uint64_t * rp;
   uint64_t high;
   uint64_t retval, h;
-  struct __lsld_ext_result struct_res;
+  struct __lsld64_result struct_res;
   uint64_t low;
   int32_t i;
   uint64_t l, h1;
-  struct __lsld_ext_result struct_res1;
+  struct __lsld64_result struct_res1;
   tnc = UINT64_C(64) - cnt;
   msb = sz - 1;
   xp = x + 0;
   rp = r + 0;
   high = *xp;
-  struct_res = lsld_ext(high, tnc);
+  struct_res = lsld64(high, tnc);
   retval = struct_res.__field_0;
   h = struct_res.__field_1;
   low = h;
@@ -59,7 +59,7 @@ uint64_t wmpn_rshift1(uint64_t * r, uint64_t * x, int32_t sz, uint64_t cnt) {
   while (i < msb) {
     xp = xp + 1;
     high = *xp;
-    struct_res1 = lsld_ext(high, tnc);
+    struct_res1 = lsld64(high, tnc);
     l = struct_res1.__field_0;
     h1 = struct_res1.__field_1;
     *rp = low + l;
@@ -77,20 +77,20 @@ uint64_t wmpn_lshift_in_place(uint64_t * x, int32_t sz, uint64_t cnt) {
   uint64_t high, low;
   int32_t i;
   uint64_t l, retval, l1, h;
-  struct __lsld_ext_result struct_res, struct_res1;
+  struct __lsld64_result struct_res, struct_res1;
   msb = sz - 1;
   xp = x + msb;
   high = UINT64_C(0);
   low = *xp;
   i = msb;
-  struct_res = lsld_ext(low, cnt);
+  struct_res = lsld64(low, cnt);
   l = struct_res.__field_0;
   retval = struct_res.__field_1;
   high = l;
   while (i > 0) {
     xp = xp + -1;
     low = *xp;
-    struct_res1 = lsld_ext(low, cnt);
+    struct_res1 = lsld64(low, cnt);
     l1 = struct_res1.__field_0;
     h = struct_res1.__field_1;
     xp[1] = high + h;
@@ -107,16 +107,16 @@ uint64_t wmpn_rshift_in_place(uint64_t * x, int32_t sz, uint64_t cnt) {
   uint64_t * xp;
   uint64_t high;
   uint64_t retval, h;
-  struct __lsld_ext_result struct_res;
+  struct __lsld64_result struct_res;
   uint64_t low;
   int32_t i;
   uint64_t l, h1;
-  struct __lsld_ext_result struct_res1;
+  struct __lsld64_result struct_res1;
   tnc = UINT64_C(64) - cnt;
   msb = sz - 1;
   xp = x + 0;
   high = *xp;
-  struct_res = lsld_ext(high, tnc);
+  struct_res = lsld64(high, tnc);
   retval = struct_res.__field_0;
   h = struct_res.__field_1;
   low = h;
@@ -124,7 +124,7 @@ uint64_t wmpn_rshift_in_place(uint64_t * x, int32_t sz, uint64_t cnt) {
   while (i < msb) {
     xp = xp + 1;
     high = *xp;
-    struct_res1 = lsld_ext(high, tnc);
+    struct_res1 = lsld64(high, tnc);
     l = struct_res1.__field_0;
     h1 = struct_res1.__field_1;
     xp[-1] = low + l;
diff --git a/lib/logicalold.h b/lib/logicalold.h
index 0e16d33..b5ee3ed 100644
--- a/lib/logicalold.h
+++ b/lib/logicalold.h
@@ -2,7 +2,6 @@
 
 #include "uint64gmp.h"
 #include "c.h"
-#include "logicalutil.h"
 #include <stdint.h>
 
 uint64_t wmpn_lshift1(uint64_t * r, uint64_t * x, int32_t sz, uint64_t cnt);
diff --git a/lib/logicalutil.c b/lib/logicalutil.c
deleted file mode 100644
index d21d341..0000000
--- a/lib/logicalutil.c
+++ /dev/null
@@ -1,23 +0,0 @@
-#include "logicalutil.h"
-#include <stdint.h>
-struct __lsld_ext_result;
-
-
-struct __lsld_ext_result lsld_ext(uint64_t x, uint64_t cnt) {
-  struct __lsld_ext_result result;
-  uint64_t r, d;
-  struct __lsld64_result struct_res;
-  struct __lsld_ext_result result1;
-  if (cnt == UINT64_C(0)) {
-    result.__field_0 = x;
-    result.__field_1 = UINT64_C(0);
-    return result;
-  } else {
-    struct_res = lsld64(x, cnt);
-    r = struct_res.__field_0;
-    d = struct_res.__field_1;
-    result1.__field_0 = r;
-    result1.__field_1 = d;
-    return result1;
-  }
-}
diff --git a/lib/logicalutil.h b/lib/logicalutil.h
deleted file mode 100644
index a3e4d12..0000000
--- a/lib/logicalutil.h
+++ /dev/null
@@ -1,15 +0,0 @@
-#ifndef LOGICALUTIL_H_INCLUDED
-
-#include "uint64gmp.h"
-#include "c.h"
-#include <stdint.h>
-
-struct __lsld_ext_result {
-  uint64_t __field_0;
-  uint64_t __field_1;
-};
-
-struct __lsld_ext_result lsld_ext(uint64_t x, uint64_t cnt);
-
-#define LOGICALUTIL_H_INCLUDED
-#endif // LOGICALUTIL_H_INCLUDED
diff --git a/lib/powm.h b/lib/powm.h
index ee09c95..3a2e28b 100644
--- a/lib/powm.h
+++ b/lib/powm.h
@@ -9,7 +9,6 @@
 #include "addold.h"
 #include "subold.h"
 #include "mul.h"
-#include "logicalutil.h"
 #include "div.h"
 #include "toom.h"
 #include <stdint.h>
diff --git a/lib/sqrt.c b/lib/sqrt.c
index e45ffbd..c0ed498 100644
--- a/lib/sqrt.c
+++ b/lib/sqrt.c
@@ -54,7 +54,7 @@ uint64_t wmpn_dc_sqrtrem(uint64_t * sp, uint64_t * np, int32_t n,
   uint64_t * npqt;
   uint64_t * spl;
   uint64_t q;
-  uint64_t o, sl, sh;
+  uint64_t result, sl, sh;
   uint64_t * npl;
   int64_t c;
   uint64_t * nr;
@@ -63,10 +63,10 @@ uint64_t wmpn_dc_sqrtrem(uint64_t * sp, uint64_t * np, int32_t n,
   uint64_t res, st, ql, qh, cqt;
   uint64_t * npn;
   int32_t ll;
-  uint64_t bo, b, bo1, o1, cqt1;
+  uint64_t bo, b, bo1, o, cqt1;
   uint64_t * nll;
-  int64_t o2, o3;
-  uint64_t o4, bo2;
+  int64_t o1, o2;
+  uint64_t o3, bo2;
   if (n == 1) {
     r = wmpn_sqrtrem2(sp, scratch, np);
     *np = *scratch;
@@ -76,8 +76,8 @@ uint64_t wmpn_dc_sqrtrem(uint64_t * sp, uint64_t * np, int32_t n,
     h = n - l;
     npqt = np + (l + l);
     spl = sp + l;
-    o = wmpn_dc_sqrtrem(spl, npqt, h, scratch);
-    q = o;
+    result = wmpn_dc_sqrtrem(spl, npqt, h, scratch);
+    q = result;
     if (!(q == UINT64_C(0))) {
       wmpn_sub_n_in_place(npqt, spl, h);
     }
@@ -117,15 +117,15 @@ uint64_t wmpn_dc_sqrtrem(uint64_t * sp, uint64_t * np, int32_t n,
       c = c - (int64_t)bo1;
     }
     if (c < INT64_C(0)) {
-      o1 = wmpn_add_1_in_place(spl, h, q);
-      q = o1;
+      o = wmpn_add_1_in_place(spl, h, q);
+      q = o;
       IGNORE2(sp, spl);
       cqt1 = wmpn_addmul_1(np, sp, n, UINT64_C(2));
       c = c + (int64_t)(UINT64_C(2) * q + cqt1);
-      o4 = wmpn_sub_1_in_place(np, n, UINT64_C(1));
-      o3 = (int64_t)o4;
-      o2 = c - o3;
-      c = o2;
+      o3 = wmpn_sub_1_in_place(np, n, UINT64_C(1));
+      o2 = (int64_t)o3;
+      o1 = c - o2;
+      c = o1;
       bo2 = wmpn_sub_1_in_place(sp, n, UINT64_C(1));
       q = q - bo2;
     } else {
@@ -159,7 +159,7 @@ int32_t wmpn_sqrtrem(uint64_t * sp, uint64_t * rp, uint64_t * np, int32_t n) {
   uint64_t o3;
   uint64_t c2;
   uint64_t * tp11;
-  uint64_t * o4;
+  uint64_t * result;
   uint64_t * nr1;
   uint64_t * nx1;
   struct __open_shift_sep_result struct_res1;
@@ -231,12 +231,12 @@ int32_t wmpn_sqrtrem(uint64_t * sp, uint64_t * rp, uint64_t * np, int32_t n) {
       tp = tp11;
     }
     if (!(c2 == UINT64_C(0))) {
-      o4 = tp;
-      struct_res1 = open_shift_sep(rp, o4);
+      result = tp;
+      struct_res1 = open_shift_sep(rp, result);
       nr1 = struct_res1.__field_0;
       nx1 = struct_res1.__field_1;
       res2 = wmpn_rshift(nr1, nx1, tn, c2);
-      IGNORE2(rp, o4);
+      IGNORE2(rp, result);
       res2;
     } else {
       wmpn_copyi1(rp, tp, tn);
diff --git a/lib/sqrt.h b/lib/sqrt.h
index ac54276..471ab83 100644
--- a/lib/sqrt.h
+++ b/lib/sqrt.h
@@ -9,7 +9,6 @@
 #include "sub_1.h"
 #include "subold.h"
 #include "mul.h"
-#include "logicalutil.h"
 #include "logical.h"
 #include "div.h"
 #include "sqrt1.h"
diff --git a/lib/sub.c b/lib/sub.c
index 2b8291d..bcf6364 100644
--- a/lib/sub.c
+++ b/lib/sub.c
@@ -26,11 +26,11 @@ uint64_t wmpn_sub_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
 uint64_t wmpn_sub(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
                   int32_t sy) {
   uint64_t lx, b;
-  uint64_t o, res;
+  uint64_t result, res;
   int32_t i;
   lx = UINT64_C(0);
-  o = wmpn_sub_n(r, x, y, sy);
-  b = o;
+  result = wmpn_sub_n(r, x, y, sy);
+  b = result;
   i = sy;
   if (!(b == UINT64_C(0))) {
     while (i < sx) {
diff --git a/lib/subold.c b/lib/subold.c
index 9f59f97..cedc979 100644
--- a/lib/subold.c
+++ b/lib/subold.c
@@ -26,11 +26,11 @@ uint64_t wmpn_sub_n1(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
 uint64_t wmpn_sub1(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
                    int32_t sy) {
   uint64_t lx, b;
-  uint64_t o, res;
+  uint64_t result, res;
   int32_t i;
   lx = UINT64_C(0);
-  o = wmpn_sub_n1(r, x, y, sy);
-  b = o;
+  result = wmpn_sub_n1(r, x, y, sy);
+  b = result;
   i = sy;
   if (!(b == UINT64_C(0))) {
     while (i < sx) {
@@ -76,11 +76,11 @@ uint64_t wmpn_sub_n_in_place(uint64_t * x, uint64_t * y, int32_t sz) {
 
 uint64_t wmpn_sub_in_place(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
   uint64_t lx, b;
-  uint64_t o, res;
+  uint64_t result, res;
   int32_t i;
   lx = UINT64_C(0);
-  o = wmpn_sub_n_in_place(x, y, sy);
-  b = o;
+  result = wmpn_sub_n_in_place(x, y, sy);
+  b = result;
   i = sy;
   if (!(b == UINT64_C(0))) {
     while (i < sx) {
diff --git a/lib/toom.c b/lib/toom.c
index b91085f..ecc56c2 100644
--- a/lib/toom.c
+++ b/lib/toom.c
@@ -41,7 +41,7 @@ void wmpn_toom22_mul(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
   uint64_t * v0n;
   uint64_t * vinfn;
   uint64_t cy;
-  uint64_t o, c, cy2, cqt, cqtqt, b1;
+  uint64_t result, c, cy2, cqt, cqtqt, b1;
   uint64_t * vinf0;
   uint64_t * vinfn1;
   s = sx / 2;
@@ -108,8 +108,8 @@ void wmpn_toom22_mul(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
   wmpn_toom22_mul_n_rec(v0, x0, y0, s_out, n);
   v0n = v0 + n;
   vinfn = vinf + n;
-  o = wmpn_add_n_in_place(vinf, v0n, n);
-  cy = o;
+  result = wmpn_add_n_in_place(vinf, v0n, n);
+  cy = result;
   c = wmpn_add_n1(v0n, vinf, v0, n);
   cy2 = c + cy;
   cqt = wmpn_add_in_place(vinf, n, vinfn, s + t - n);
@@ -186,7 +186,7 @@ void wmpn_toom32_mul(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
   uint64_t * vm1;
   uint64_t xp1_hi, yp1_hi, hi;
   int vm1_neg;
-  uint64_t o, b, c, o1, o2;
+  uint64_t result, b, c, result1, result2;
   int32_t cmp, cmp1;
   uint64_t * y0t;
   int c0, c1;
@@ -241,8 +241,8 @@ void wmpn_toom32_mul(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
   yp1_hi = UINT64_C(0);
   hi = UINT64_C(0);
   vm1_neg = 0;
-  o = wmpn_add1(xp1, x0, n, x2, s);
-  xp1_hi = o;
+  result = wmpn_add1(xp1, x0, n, x2, s);
+  xp1_hi = result;
   cmp = wmpn_cmp(xp1, x1, n);
   if (xp1_hi == UINT64_C(0) && cmp < 0) {
     wmpn_sub_n1(xm1, x1, xp1, n);
@@ -255,8 +255,8 @@ void wmpn_toom32_mul(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
   c = wmpn_add_n_in_place(xp1, x1, n);
   xp1_hi = xp1_hi + c;
   if (t == n) {
-    o1 = wmpn_add_n1(yp1, y0, y1, n);
-    yp1_hi = o1;
+    result1 = wmpn_add_n1(yp1, y0, y1, n);
+    yp1_hi = result1;
     cmp1 = wmpn_cmp(y0, y1, n);
     if (cmp1 < 0) {
       wmpn_sub_n1(ym1, y1, y0, n);
@@ -265,8 +265,8 @@ void wmpn_toom32_mul(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
       wmpn_sub_n1(ym1, y0, y1, n);
     }
   } else {
-    o2 = wmpn_add1(yp1, y0, n, y1, t);
-    yp1_hi = o2;
+    result2 = wmpn_add1(yp1, y0, n, y1, t);
+    yp1_hi = result2;
     y0t = y0 + t;
     c0 = wmpn_zero_p(y0t, n - t) == 1;
     cmp2 = wmpn_cmp(y0, y1, t);
diff --git a/lib/zadd.c b/lib/zadd.c
index 7139963..61a3b89 100644
--- a/lib/zadd.c
+++ b/lib/zadd.c
@@ -303,7 +303,7 @@ void wmpz_add_ui(wmpz_ptr w, wmpz_ptr u, uint64_t v) {
   int32_t wsize;
   uint64_t * wp1;
   uint64_t cy;
-  uint64_t o, o1;
+  uint64_t result, result1;
   uint64_t * up;
   uint64_t * up1;
   usize = SIZ(u);
@@ -325,12 +325,12 @@ void wmpz_add_ui(wmpz_ptr w, wmpz_ptr u, uint64_t v) {
   cy = UINT64_C(0);
   if (usize >= 0) {
     if (uw) {
-      o = wmpn_add_1_in_place(wp1, abs_usize, v);
-      cy = o;
+      result = wmpn_add_1_in_place(wp1, abs_usize, v);
+      cy = result;
     } else {
       up = PTR(u);
-      o1 = wmpn_add_1(wp1, up, abs_usize, v);
-      cy = o1;
+      result1 = wmpn_add_1(wp1, up, abs_usize, v);
+      cy = result1;
       (void)(u);
     }
     wp1[abs_usize] = cy;
diff --git a/lib/zdiv.c b/lib/zdiv.c
index 3c9e59b..68e017a 100644
--- a/lib/zdiv.c
+++ b/lib/zdiv.c
@@ -102,7 +102,7 @@ uint64_t wmpz_tdiv_qr_ui(wmpz_ptr quot, wmpz_ptr rem, wmpz_ptr dividend,
   int32_t qn;
   uint64_t rl;
   uint64_t * np;
-  uint64_t o, o1;
+  uint64_t result, result1;
   uint64_t * np1;
   int32_t rs;
   uint64_t * rp;
@@ -125,12 +125,12 @@ uint64_t wmpz_tdiv_qr_ui(wmpz_ptr quot, wmpz_ptr rem, wmpz_ptr dividend,
   if (quot == dividend) {
     np = alloca((uint32_t)nn * sizeof(uint64_t));
     wmpn_copyd_sep(np, qp, nn);
-    o = wmpn_divrem_1(qp, np, nn, divisor);
-    rl = o;
+    result = wmpn_divrem_1(qp, np, nn, divisor);
+    rl = result;
   } else {
     np1 = PTR(dividend);
-    o1 = wmpn_divrem_1(qp, np1, nn, divisor);
-    rl = o1;
+    result1 = wmpn_divrem_1(qp, np1, nn, divisor);
+    rl = result1;
     (void)(dividend);
   }
   if (rl == UINT64_C(0)) {
diff --git a/lib/zdiv2exp.h b/lib/zdiv2exp.h
index e18a678..b1c82a0 100644
--- a/lib/zdiv2exp.h
+++ b/lib/zdiv2exp.h
@@ -6,7 +6,6 @@
 #include "alias.h"
 #include "compare.h"
 #include "uint64gmp.h"
-#include "logicalutil.h"
 #include "logical.h"
 #include "logicalold.h"
 #include "z.h"
diff --git a/lib/zmul2exp.c b/lib/zmul2exp.c
index bd7a9a5..bc4480f 100644
--- a/lib/zmul2exp.c
+++ b/lib/zmul2exp.c
@@ -1,7 +1,7 @@
 #include "zmul2exp.h"
 #include <stdint.h>
 
-void wmpz_mul2exp(wmpz_ptr r, wmpz_ptr u, uint64_t cnt) {
+void wmpz_mul_2exp(wmpz_ptr r, wmpz_ptr u, uint64_t cnt) {
   int32_t un, limb_cnt;
   int32_t rn;
   uint64_t * rp;
diff --git a/lib/zmul2exp.h b/lib/zmul2exp.h
index 37d42fb..d8756a2 100644
--- a/lib/zmul2exp.h
+++ b/lib/zmul2exp.h
@@ -6,14 +6,13 @@
 #include "alias.h"
 #include "compare.h"
 #include "uint64gmp.h"
-#include "logicalutil.h"
 #include "logical.h"
 #include "logicalold.h"
 #include "z.h"
 #include "zutil.h"
 #include <stdint.h>
 
-void wmpz_mul2exp(wmpz_ptr r, wmpz_ptr u, uint64_t cnt);
+void wmpz_mul_2exp(wmpz_ptr r, wmpz_ptr u, uint64_t cnt);
 
 #define ZMUL2EXP_H_INCLUDED
 #endif // ZMUL2EXP_H_INCLUDED
diff --git a/lib/zneg.c b/lib/zneg.c
new file mode 100644
index 0000000..4968377
--- /dev/null
+++ b/lib/zneg.c
@@ -0,0 +1,26 @@
+#include "zneg.h"
+#include <stdint.h>
+
+void wmpz_neg(wmpz_ptr w, wmpz_ptr u) {
+  int32_t usize, wsize, size;
+  uint64_t * wp;
+  uint64_t * up;
+  usize = SIZ(u);
+  wsize = -usize;
+  if (!(u == w)) {
+    if (usize >= 0) {
+      size = usize;
+    } else {
+      size = -usize;
+    }
+    wp = wmpz_realloc(w, size);
+    up = PTR(u);
+    wmpn_copyd_sep(wp, up, size);
+    (void)(u);
+    SIZ(w) = wsize;
+    (void)(w);
+    return;
+  } else {
+    return;
+  }
+}
diff --git a/lib/zneg.h b/lib/zneg.h
new file mode 100644
index 0000000..df7955a
--- /dev/null
+++ b/lib/zneg.h
@@ -0,0 +1,14 @@
+#ifndef ZNEG_H_INCLUDED
+
+#include "c.h"
+#include "util.h"
+#include "compare.h"
+#include "uint64gmp.h"
+#include "z.h"
+#include "zutil.h"
+#include <stdint.h>
+
+void wmpz_neg(wmpz_ptr w, wmpz_ptr u);
+
+#define ZNEG_H_INCLUDED
+#endif // ZNEG_H_INCLUDED
diff --git a/lib/zrealloc2.c b/lib/zrealloc2.c
new file mode 100644
index 0000000..f9090aa
--- /dev/null
+++ b/lib/zrealloc2.c
@@ -0,0 +1,18 @@
+#include "zrealloc2.h"
+#include <stdint.h>
+
+void wmpz_realloc2(wmpz_ptr x, uint64_t bits) {
+  uint64_t bits1;
+  int32_t new_alloc;
+  uint64_t * p;
+  uint64_t * q;
+  bits1 = bits - !(bits == UINT64_C(0));
+  new_alloc = (int32_t)(UINT64_C(1) + bits1 / UINT64_C(64));
+  p = PTR(x);
+  q = realloc(p, new_alloc * sizeof(uint64_t));
+  assert (q);
+  ALLOC(x) = new_alloc;
+  PTR(x) = q;
+  (void)(x);
+  return;
+}
diff --git a/lib/zrealloc2.h b/lib/zrealloc2.h
new file mode 100644
index 0000000..0c7dbdf
--- /dev/null
+++ b/lib/zrealloc2.h
@@ -0,0 +1,14 @@
+#ifndef ZREALLOC2_H_INCLUDED
+
+#include "c.h"
+#include "util.h"
+#include "compare.h"
+#include "uint64gmp.h"
+#include "z.h"
+#include "zutil.h"
+#include <stdint.h>
+
+void wmpz_realloc2(wmpz_ptr x, uint64_t bits);
+
+#define ZREALLOC2_H_INCLUDED
+#endif // ZREALLOC2_H_INCLUDED
diff --git a/lib/zsub.c b/lib/zsub.c
index 2328dd7..41a2ab9 100644
--- a/lib/zsub.c
+++ b/lib/zsub.c
@@ -302,7 +302,7 @@ void wmpz_sub_ui(wmpz_ptr w, wmpz_ptr u, uint64_t v) {
   int32_t wsize;
   uint64_t * wp1;
   uint64_t cy;
-  uint64_t o, o1;
+  uint64_t result, result1;
   uint64_t * up;
   uint64_t * up1;
   usize = SIZ(u);
@@ -324,12 +324,12 @@ void wmpz_sub_ui(wmpz_ptr w, wmpz_ptr u, uint64_t v) {
   cy = UINT64_C(0);
   if (usize < 0) {
     if (uw) {
-      o = wmpn_add_1_in_place(wp1, abs_usize, v);
-      cy = o;
+      result = wmpn_add_1_in_place(wp1, abs_usize, v);
+      cy = result;
     } else {
       up = PTR(u);
-      o1 = wmpn_add_1(wp1, up, abs_usize, v);
-      cy = o1;
+      result1 = wmpn_add_1(wp1, up, abs_usize, v);
+      cy = result1;
       (void)(u);
     }
     wp1[abs_usize] = cy;
diff --git a/why3 b/why3
index 2a35b57..9e120d4 160000
--- a/why3
+++ b/why3
@@ -1 +1 @@
-Subproject commit 2a35b574eba191bed7953b6d9fc6ffb4c417ab0b
+Subproject commit 9e120d4fbcbb42ee95aa5acafa801e0a419a74e9
-- 
GitLab