diff --git a/projects/int_array.strategies b/projects/int_array.strategies
old mode 100644
new mode 100755
diff --git a/projects/int_array_def.h b/projects/int_array_def.h
old mode 100644
new mode 100755
diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v
index 787c79e..21db244 100755
--- a/projects/lib/GmpNumber.v
+++ b/projects/lib/GmpNumber.v
@@ -597,20 +597,10 @@ Record bigint_ent: Type := {
     sign: Prop;
 }.
 
-Definition store_bigint_ent (x: addr) (n: bigint_ent): Assertion :=
-    EX size, 
-      &(x # "__mpz_struct" ->ₛ "_mp_size") # Int |-> size &&
-      ([| size < 0 |] && [| sign n |] && [| size = -Zlength (data n) |] ||
-        [| size >= 0 |] && [| ~(sign n) |] && [| size = Zlength (data n) |]) **
-    &(x # "__mpz_struct" ->ₛ "_mp_alloc") # Int |-> cap n **
-    EX p, 
-      &(x # "__mpz_struct" ->ₛ "_mp_d") # Ptr |-> p **
-    Internal.mpd_store_list p (data n) (cap n).
-
-Definition bigint_ent_store_Z (n: bigint_ent) (x: Z): Assertion :=
-  [| sign n |] && [| Internal.list_store_Z (data n) (-x) |] ||
-    [| ~(sign n) |] && [| Internal.list_store_Z (data n) x |].
-
 Definition store_Z (x: addr) (n: Z): Assertion :=
-  EX ent,
-    store_bigint_ent x ent && bigint_ent_store_Z ent n.
\ No newline at end of file
+  EX (ptr: addr) (cap size: Z),
+    (([| size < 0 |] && [| n < 0 |] && Internal.mpd_store_Z_compact ptr (-n) (-size) cap) ||
+      ([| size >= 0 |] && [| n >= 0 |] && Internal.mpd_store_Z_compact ptr n size cap)) **
+    &(x # "__mpz_struct" ->ₛ "_mp_size") # Int |-> size **
+    &(x # "__mpz_struct" ->ₛ "_mp_alloc") # Int |-> cap **
+    &(x # "__mpz_struct" ->ₛ "_mp_d") # Ptr |-> ptr.
\ No newline at end of file
diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v
old mode 100644
new mode 100755
index bbb692e..a70468a
--- a/projects/lib/gmp_goal.v
+++ b/projects/lib/gmp_goal.v
@@ -1753,6 +1753,1034 @@ forall (xp_pre: Z) (val: Z) (cap: Z) (n: Z) ,
   **  (store_undef_uint_array_rec xp_pre n cap )
 .
 
+(*----- Function mpz_clear -----*)
+
+Definition mpz_clear_return_wit_1_1 := 
+forall (r_pre: Z) (n: Z) (ptr_2: Z) (cap_2: Z) (size_2: Z) ,
+  [| (cap_2 = 0) |] 
+  &&  [| (size_2 < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_2 (-n) (-size_2) cap_2 )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_2)
+|--
+  EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_clear_return_wit_1_2 := 
+forall (r_pre: Z) (n: Z) (ptr_2: Z) (cap_2: Z) (size_2: Z) ,
+  [| (cap_2 = 0) |] 
+  &&  [| (size_2 >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_2 n size_2 cap_2 )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_2)
+|--
+  EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_clear_return_wit_1_3 := 
+forall (r_pre: Z) (n: Z) (ptr_2: Z) (cap_2: Z) (size_2: Z) ,
+  [| (cap_2 <> 0) |] 
+  &&  [| (size_2 >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_2)
+|--
+  EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_clear_return_wit_1_4 := 
+forall (r_pre: Z) (n: Z) (ptr_2: Z) (cap_2: Z) (size_2: Z) ,
+  [| (cap_2 <> 0) |] 
+  &&  [| (size_2 < 0) |] 
+  &&  [| (n < 0) |]
+  &&  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_2)
+|--
+  EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_clear_partial_solve_wit_1 := 
+forall (r_pre: Z) (n: Z) ,
+  (store_Z r_pre n )
+|--
+  (store_Z r_pre n )
+.
+
+Definition mpz_clear_partial_solve_wit_2 := 
+forall (r_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (cap <> 0) |] 
+  &&  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_clear_partial_solve_wit_3 := 
+forall (r_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (cap <> 0) |] 
+  &&  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_clear_which_implies_wit_1 := 
+forall (r_pre: Z) (n: Z) ,
+  (store_Z r_pre n )
+|--
+  (EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  [| (size >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n size cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr))
+  ||
+  (EX (ptr: Z)  (cap: Z)  (size: Z) ,
+  [| (size < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-size) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> size)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr))
+.
+
+(*----- Function mpz_realloc -----*)
+
+Definition mpz_realloc_safety_wit_1 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) ,
+  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  ((( &( "size" ) )) # Int  |-> size_pre)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (1 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 1) |]
+.
+
+Definition mpz_realloc_safety_wit_2 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) ,
+  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  ((( &( "size" ) )) # Int  |-> size_pre)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (1 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 1) |]
+.
+
+Definition mpz_realloc_safety_wit_3 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (store_undef_uint_array retval_3 retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpz_realloc_safety_wit_4 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (store_undef_uint_array retval_3 retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpz_realloc_safety_wit_5 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact retval_3 (-n) (-old) retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpz_realloc_safety_wit_6 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact retval_3 n old retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  [| (0 <= INT_MAX) |] 
+  &&  [| ((INT_MIN) <= 0) |]
+.
+
+Definition mpz_realloc_return_wit_1_1 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval <= retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact retval_3 n old retval_2 )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_return_wit_1_2 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval <= retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact retval_3 (-n) (-old) retval_2 )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_return_wit_1_3 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval <= retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (store_undef_uint_array retval_3 retval_2 )
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_return_wit_1_4 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval <= retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (store_undef_uint_array retval_3 retval_2 )
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_return_wit_1_5 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (store_undef_uint_array retval_3 retval_2 )
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> 0)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_return_wit_1_6 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (store_undef_uint_array retval_3 retval_2 )
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> 0)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_return_wit_1_7 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact retval_3 (-n) (-old) retval_2 )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> 0)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_return_wit_1_8 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3: Z) (retval: Z) ,
+  [| (retval > retval_2) |] 
+  &&  [| (retval = (Zabs (old))) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact retval_3 n old retval_2 )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> 0)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_3)
+|--
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr_new (-n) (-old) c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+  ||
+  (EX (ptr_new: Z)  (c: Z) ,
+  [| (c >= size_pre) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr_new n old c )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> c)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr_new))
+.
+
+Definition mpz_realloc_partial_solve_wit_1 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) ,
+  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_realloc_partial_solve_wit_2 := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) ,
+  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_realloc_partial_solve_wit_3_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  ((( &( "size" ) )) # Int  |-> retval)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (cap >= 0) |] 
+  &&  [| (retval >= cap) |] 
+  &&  [| ((Zmax (size_pre) (1)) >= cap) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_3_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (cap >= 0) |] 
+  &&  [| (retval >= cap) |] 
+  &&  [| ((Zmax (size_pre) (1)) >= cap) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_realloc_partial_solve_wit_3 := mpz_realloc_partial_solve_wit_3_pure -> mpz_realloc_partial_solve_wit_3_aux.
+
+Definition mpz_realloc_partial_solve_wit_4_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  ((( &( "size" ) )) # Int  |-> retval)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (cap >= 0) |] 
+  &&  [| (retval >= cap) |] 
+  &&  [| ((Zmax (size_pre) (1)) >= cap) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_4_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (cap >= 0) |] 
+  &&  [| (retval >= cap) |] 
+  &&  [| ((Zmax (size_pre) (1)) >= cap) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_realloc_partial_solve_wit_4 := mpz_realloc_partial_solve_wit_4_pure -> mpz_realloc_partial_solve_wit_4_aux.
+
+Definition mpz_realloc_partial_solve_wit_5_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  ((( &( "size" ) )) # Int  |-> retval)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (retval >= 0) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_5_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (retval >= 0) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_realloc_partial_solve_wit_5 := mpz_realloc_partial_solve_wit_5_pure -> mpz_realloc_partial_solve_wit_5_aux.
+
+Definition mpz_realloc_partial_solve_wit_6_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  ((( &( "size" ) )) # Int  |-> retval)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (retval >= 0) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_6_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+|--
+  [| (retval >= 0) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> cap)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> ptr)
+.
+
+Definition mpz_realloc_partial_solve_wit_6 := mpz_realloc_partial_solve_wit_6_pure -> mpz_realloc_partial_solve_wit_6_aux.
+
+Definition mpz_realloc_partial_solve_wit_7_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (store_undef_uint_array retval retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval)
+|--
+  [| (old <= INT_MAX) |] 
+  &&  [| (INT_MIN < old) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_7_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) (retval_2: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (store_undef_uint_array retval_2 retval )
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+|--
+  [| (old <= INT_MAX) |] 
+  &&  [| (INT_MIN < old) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (store_undef_uint_array retval_2 retval )
+  **  (mpd_store_Z_compact ptr (-n) (-old) cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+.
+
+Definition mpz_realloc_partial_solve_wit_7 := mpz_realloc_partial_solve_wit_7_pure -> mpz_realloc_partial_solve_wit_7_aux.
+
+Definition mpz_realloc_partial_solve_wit_8_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (store_undef_uint_array retval retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval)
+|--
+  [| (INT_MIN < old) |] 
+  &&  [| (old <= INT_MAX) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_8_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) (retval_2: Z) ,
+  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (store_undef_uint_array retval_2 retval )
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+|--
+  [| (INT_MIN < old) |] 
+  &&  [| (old <= INT_MAX) |] 
+  &&  [| (cap = 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (store_undef_uint_array retval_2 retval )
+  **  (mpd_store_Z_compact ptr n old cap )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+.
+
+Definition mpz_realloc_partial_solve_wit_8 := mpz_realloc_partial_solve_wit_8_pure -> mpz_realloc_partial_solve_wit_8_aux.
+
+Definition mpz_realloc_partial_solve_wit_9_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact retval (-n) (-old) retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval)
+|--
+  [| (old <= INT_MAX) |] 
+  &&  [| (INT_MIN < old) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_9_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact retval_2 (-n) (-old) retval )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+|--
+  [| (old <= INT_MAX) |] 
+  &&  [| (INT_MIN < old) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old < 0) |] 
+  &&  [| (n < 0) |]
+  &&  (mpd_store_Z_compact retval_2 (-n) (-old) retval )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+.
+
+Definition mpz_realloc_partial_solve_wit_9 := mpz_realloc_partial_solve_wit_9_pure -> mpz_realloc_partial_solve_wit_9_aux.
+
+Definition mpz_realloc_partial_solve_wit_10_pure := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval_2 = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact retval n old retval_2 )
+  **  ((( &( "size" ) )) # Int  |-> retval_2)
+  **  ((( &( "r" ) )) # Ptr  |-> r_pre)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval_2)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval)
+|--
+  [| (INT_MIN < old) |] 
+  &&  [| (old <= INT_MAX) |]
+.
+
+Definition mpz_realloc_partial_solve_wit_10_aux := 
+forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2: Z) ,
+  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact retval_2 n old retval )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+|--
+  [| (INT_MIN < old) |] 
+  &&  [| (old <= INT_MAX) |] 
+  &&  [| (cap <> 0) |] 
+  &&  [| (retval = (Zmax (size_pre) (1))) |] 
+  &&  [| (size_pre >= cap) |] 
+  &&  [| (size_pre <= 100000000) |] 
+  &&  [| (cap >= 0) |] 
+  &&  [| (cap <= 100000000) |] 
+  &&  [| (old >= 0) |] 
+  &&  [| (n >= 0) |]
+  &&  (mpd_store_Z_compact retval_2 n old retval )
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_size")) # Int  |-> old)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_alloc")) # Int  |-> retval)
+  **  ((&((r_pre)  # "__mpz_struct" ->ₛ "_mp_d")) # Ptr  |-> retval_2)
+.
+
+Definition mpz_realloc_partial_solve_wit_10 := mpz_realloc_partial_solve_wit_10_pure -> mpz_realloc_partial_solve_wit_10_aux.
+
 Module Type VC_Correct.
 
 Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1.
@@ -1823,5 +2851,45 @@ Axiom proof_of_mpn_normalized_size_return_wit_1_2 : mpn_normalized_size_return_w
 Axiom proof_of_mpn_normalized_size_partial_solve_wit_1 : mpn_normalized_size_partial_solve_wit_1.
 Axiom proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2.
 Axiom proof_of_mpn_normalized_size_which_implies_wit_1 : mpn_normalized_size_which_implies_wit_1.
+Axiom proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1.
+Axiom proof_of_mpz_clear_return_wit_1_2 : mpz_clear_return_wit_1_2.
+Axiom proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3.
+Axiom proof_of_mpz_clear_return_wit_1_4 : mpz_clear_return_wit_1_4.
+Axiom proof_of_mpz_clear_partial_solve_wit_1 : mpz_clear_partial_solve_wit_1.
+Axiom proof_of_mpz_clear_partial_solve_wit_2 : mpz_clear_partial_solve_wit_2.
+Axiom proof_of_mpz_clear_partial_solve_wit_3 : mpz_clear_partial_solve_wit_3.
+Axiom proof_of_mpz_clear_which_implies_wit_1 : mpz_clear_which_implies_wit_1.
+Axiom proof_of_mpz_realloc_safety_wit_1 : mpz_realloc_safety_wit_1.
+Axiom proof_of_mpz_realloc_safety_wit_2 : mpz_realloc_safety_wit_2.
+Axiom proof_of_mpz_realloc_safety_wit_3 : mpz_realloc_safety_wit_3.
+Axiom proof_of_mpz_realloc_safety_wit_4 : mpz_realloc_safety_wit_4.
+Axiom proof_of_mpz_realloc_safety_wit_5 : mpz_realloc_safety_wit_5.
+Axiom proof_of_mpz_realloc_safety_wit_6 : mpz_realloc_safety_wit_6.
+Axiom proof_of_mpz_realloc_return_wit_1_1 : mpz_realloc_return_wit_1_1.
+Axiom proof_of_mpz_realloc_return_wit_1_2 : mpz_realloc_return_wit_1_2.
+Axiom proof_of_mpz_realloc_return_wit_1_3 : mpz_realloc_return_wit_1_3.
+Axiom proof_of_mpz_realloc_return_wit_1_4 : mpz_realloc_return_wit_1_4.
+Axiom proof_of_mpz_realloc_return_wit_1_5 : mpz_realloc_return_wit_1_5.
+Axiom proof_of_mpz_realloc_return_wit_1_6 : mpz_realloc_return_wit_1_6.
+Axiom proof_of_mpz_realloc_return_wit_1_7 : mpz_realloc_return_wit_1_7.
+Axiom proof_of_mpz_realloc_return_wit_1_8 : mpz_realloc_return_wit_1_8.
+Axiom proof_of_mpz_realloc_partial_solve_wit_1 : mpz_realloc_partial_solve_wit_1.
+Axiom proof_of_mpz_realloc_partial_solve_wit_2 : mpz_realloc_partial_solve_wit_2.
+Axiom proof_of_mpz_realloc_partial_solve_wit_3_pure : mpz_realloc_partial_solve_wit_3_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_3 : mpz_realloc_partial_solve_wit_3.
+Axiom proof_of_mpz_realloc_partial_solve_wit_4_pure : mpz_realloc_partial_solve_wit_4_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_4 : mpz_realloc_partial_solve_wit_4.
+Axiom proof_of_mpz_realloc_partial_solve_wit_5_pure : mpz_realloc_partial_solve_wit_5_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_5 : mpz_realloc_partial_solve_wit_5.
+Axiom proof_of_mpz_realloc_partial_solve_wit_6_pure : mpz_realloc_partial_solve_wit_6_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_6 : mpz_realloc_partial_solve_wit_6.
+Axiom proof_of_mpz_realloc_partial_solve_wit_7_pure : mpz_realloc_partial_solve_wit_7_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_7 : mpz_realloc_partial_solve_wit_7.
+Axiom proof_of_mpz_realloc_partial_solve_wit_8_pure : mpz_realloc_partial_solve_wit_8_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_8 : mpz_realloc_partial_solve_wit_8.
+Axiom proof_of_mpz_realloc_partial_solve_wit_9_pure : mpz_realloc_partial_solve_wit_9_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_9 : mpz_realloc_partial_solve_wit_9.
+Axiom proof_of_mpz_realloc_partial_solve_wit_10_pure : mpz_realloc_partial_solve_wit_10_pure.
+Axiom proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10.
 
 End VC_Correct.
diff --git a/projects/lib/gmp_goal_check.v b/projects/lib/gmp_goal_check.v
old mode 100644
new mode 100755
diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v
old mode 100644
new mode 100755
index 153a2b3..d7e29ef
--- a/projects/lib/gmp_proof_auto.v
+++ b/projects/lib/gmp_proof_auto.v
@@ -141,3 +141,66 @@ Proof. Admitted.
 Lemma proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2.
 Proof. Admitted. 
 
+Lemma proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_return_wit_1_4 : mpz_clear_return_wit_1_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_partial_solve_wit_1 : mpz_clear_partial_solve_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_partial_solve_wit_2 : mpz_clear_partial_solve_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_clear_partial_solve_wit_3 : mpz_clear_partial_solve_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_1 : mpz_realloc_safety_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_2 : mpz_realloc_safety_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_3 : mpz_realloc_safety_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_4 : mpz_realloc_safety_wit_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_5 : mpz_realloc_safety_wit_5.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_safety_wit_6 : mpz_realloc_safety_wit_6.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_1 : mpz_realloc_partial_solve_wit_1.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_2 : mpz_realloc_partial_solve_wit_2.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_3 : mpz_realloc_partial_solve_wit_3.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_4 : mpz_realloc_partial_solve_wit_4.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_5 : mpz_realloc_partial_solve_wit_5.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_6 : mpz_realloc_partial_solve_wit_6.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_7 : mpz_realloc_partial_solve_wit_7.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_8 : mpz_realloc_partial_solve_wit_8.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_9 : mpz_realloc_partial_solve_wit_9.
+Proof. Admitted. 
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10.
+Proof. Admitted. 
+
diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v
old mode 100644
new mode 100755
index 8aedbd0..2e51564
--- a/projects/lib/gmp_proof_manual.v
+++ b/projects/lib/gmp_proof_manual.v
@@ -410,4 +410,299 @@ Proof.
     entailer!.
   + rewrite sublist_self; try lia.
     tauto.
-Qed.
\ No newline at end of file
+Qed.
+
+
+Lemma proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+  unfold mpd_store_Z_compact.
+  Intros data.
+  unfold mpd_store_list.
+  subst.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_clear_return_wit_1_2 : mpz_clear_return_wit_1_2.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+  unfold mpd_store_Z_compact.
+  Intros data.
+  unfold mpd_store_list.
+  entailer!.
+  assert (size_2 = 0). {
+    pose proof (Zlength_nonneg data).
+    lia.
+  }
+  rewrite H6 in *.
+  rewrite <-H3 in *.
+  unfold store_uint_array, store_undef_uint_array_rec.
+  unfold store_array.
+  assert (cap_2 - 0 = 0). { lia. }
+  rewrite H7; clear H7.
+  pose proof (Zlength_nil_inv data ltac:(lia)).
+  rewrite H7 in *; clear H7.
+  simpl.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+Qed.
+
+
+Lemma proof_of_mpz_clear_return_wit_1_4 : mpz_clear_return_wit_1_4.
+Proof.
+  pre_process.
+  Exists ptr_2 cap_2 size_2.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_clear_which_implies_wit_1 : mpz_clear_which_implies_wit_1.
+Proof.
+  pre_process.
+  unfold store_Z.
+  Intros ptr cap size.
+  entailer!.
+  rewrite orp_sepcon_left.
+  Split.
+  + Right.
+    Exists ptr cap size.
+    entailer!.
+  + Left.
+    Exists ptr cap size.
+    entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_1 : mpz_realloc_return_wit_1_1.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  entailer!.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_2 : mpz_realloc_return_wit_1_2.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  entailer!.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_3 : mpz_realloc_return_wit_1_3.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  entailer!.
+  + subst.
+    unfold mpd_store_Z_compact.
+    Intros data.
+    Exists data.
+    unfold mpd_store_list, store_undef_uint_array_rec.
+    entailer!.
+    - assert (Zlength data = 0). {
+        pose proof (Zlength_nonneg data).
+        lia.
+      }
+      rewrite H8 in *.
+      simpl.
+      entailer!.
+      pose proof (Zlength_nil_inv data H8).
+      repeat subst.
+      unfold store_uint_array, store_array; simpl; entailer!.
+      unfold store_undef_uint_array, store_undef_array.
+      rewrite Z.sub_0_r.
+      reflexivity.
+    - unfold Zmax in *.
+      assert (size_pre < 1 \/ size_pre >= 1). { lia. }
+      destruct H8.
+      * rewrite (Z.max_r size_pre 1 ltac:(lia)); lia.
+      * rewrite (Z.max_l size_pre 1 ltac:(lia)); lia.
+  + pose proof (Z.le_max_l size_pre 1).
+    unfold Zmax in *.
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_4 : mpz_realloc_return_wit_1_4.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  entailer!.
+  + subst.
+    unfold mpd_store_Z_compact, mpd_store_list.
+    Intros data.
+    Exists data.
+    assert (Zlength data = 0). {
+      pose proof (Zlength_nonneg data).
+      lia.
+    }
+    rewrite H8 in *; clear H2.
+    pose proof (Zlength_nil_inv data H8).
+    rewrite H2 in *; clear H2 H8.
+    unfold store_uint_array, store_array.
+    simpl.
+    entailer!.
+  + pose proof (Z.le_max_l size_pre 1).
+    unfold Zmax in *.
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_5 : mpz_realloc_return_wit_1_5.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  entailer!.
+  + subst.
+    unfold mpd_store_Z_compact, mpd_store_list.
+    Intros data.
+    Exists data.
+    unfold store_uint_array, store_array.
+    simpl.
+    entailer!.
+  + pose proof (Z.le_max_l size_pre 1).
+    unfold Zmax in *.
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_6 : mpz_realloc_return_wit_1_6.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  subst.
+  entailer!.
+  + unfold mpd_store_Z_compact, mpd_store_list.
+    Intros data; Exists data.
+    unfold store_uint_array, store_array.
+    assert (Zlength data = 0). {
+      pose proof (Zlength_nonneg data).
+      lia.
+    }
+    rewrite H8 in *; clear H2.
+    pose proof (Zlength_nil_inv data H8).
+    rewrite H2 in *; clear H2 H8.
+    unfold store_undef_uint_array, store_undef_uint_array_rec, store_undef_array.
+    subst.
+    simpl.
+    entailer!.
+    - rewrite Z.sub_0_r.
+      entailer!.
+    - pose proof (Z.le_max_r size_pre 1).
+      simpl in H.
+      unfold Zmax in *.
+      lia.
+  + unfold Zmax in *.
+    pose proof (Z.le_max_l size_pre 1).
+    lia.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_7 : mpz_realloc_return_wit_1_7.
+Proof.
+  pre_process.
+  Left.
+  Exists retval_3 retval_2.
+  subst.
+  unfold Zmax in *.
+  rewrite (Z.abs_neq old ltac:(lia)) in H.
+  pose proof (Z.le_max_l size_pre 1).
+  unfold mpd_store_Z_compact.
+  Intros data; entailer!.
+  unfold mpd_store_list.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_return_wit_1_8 : mpz_realloc_return_wit_1_8.
+Proof.
+  pre_process.
+  Right.
+  Exists retval_3 retval_2.
+  subst.
+  unfold Zmax in *.
+  rewrite (Z.abs_eq old ltac:(lia)) in H.
+  pose proof (Z.le_max_l size_pre 1).
+  unfold mpd_store_Z_compact.
+  Intros data; entailer!.
+  unfold mpd_store_list.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_3_pure : mpz_realloc_partial_solve_wit_3_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_4_pure : mpz_realloc_partial_solve_wit_4_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_5_pure : mpz_realloc_partial_solve_wit_5_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_6_pure : mpz_realloc_partial_solve_wit_6_pure.
+Proof.
+  pre_process.
+  unfold Zmax in *.
+  pose proof (Z.le_max_l size_pre 1).
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_7_pure : mpz_realloc_partial_solve_wit_7_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_8_pure : mpz_realloc_partial_solve_wit_8_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_9_pure : mpz_realloc_partial_solve_wit_9_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.
+
+Lemma proof_of_mpz_realloc_partial_solve_wit_10_pure : mpz_realloc_partial_solve_wit_10_pure.
+Proof.
+  pre_process.
+  unfold mpd_store_Z_compact, mpd_store_list.
+  Intros data.
+  entailer!.
+Qed.
diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c
index 8b9dd25..a60ffba 100755
--- a/projects/mini-gmp.c
+++ b/projects/mini-gmp.c
@@ -323,15 +323,53 @@ mpn_sub (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn)
 
 /* MPZ interface */
 
-/*void
+void
 mpz_clear (mpz_t r)
+/*@
+  With
+    n
+  Require
+    store_Z(r, n)
+  Ensure
+    exists size cap ptr,
+      r@pre -> _mp_size == size && r@pre -> _mp_alloc == cap && r@pre -> _mp_d == ptr
+*/
 {
+  /*@
+    store_Z(r@pre, n)
+    which implies
+    exists ptr size cap,
+      (size < 0 && n < 0 && mpd_store_Z_compact(ptr, -n, -size, cap) ||
+        size >= 0 && n >= 0 && mpd_store_Z_compact(ptr, n, size, cap)) &&
+      r@pre -> _mp_size == size &&
+      r@pre -> _mp_alloc == cap &&
+      r@pre -> _mp_d == ptr
+  */
   if (r->_mp_alloc)
     gmp_free_limbs (r->_mp_d, r->_mp_alloc);
-}*/
+}
 
-/*static unsigned int *
+static unsigned int *
 mpz_realloc (mpz_t r, int size)
+/*@
+  With
+    ptr old cap n
+  Require
+    size >= cap && size <= 100000000 && cap >= 0 && cap <= 100000000 &&
+    (old < 0 && n < 0 && mpd_store_Z_compact(ptr, -n, -old, cap) ||
+        old >= 0 && n >= 0 && mpd_store_Z_compact(ptr, n, old, cap)) &&
+      r -> _mp_size == old &&
+      r -> _mp_alloc == cap &&
+      r -> _mp_d == ptr
+  Ensure
+    exists c ptr_new,
+    c >= size@pre && 
+    (n < 0 && mpd_store_Z_compact(ptr_new, -n, -old, c) ||
+      n >= 0 && mpd_store_Z_compact(ptr_new, n, old, c)) &&
+    r -> _mp_size == old &&
+    r@pre -> _mp_alloc == c &&
+    r@pre -> _mp_d == ptr_new
+*/
 {
   size = gmp_max (size, 1);
 
@@ -345,7 +383,7 @@ mpz_realloc (mpz_t r, int size)
     r->_mp_size = 0;
 
   return r->_mp_d;
-}*/
+}
 
 /* Realloc for an mpz_t WHAT if it has less than NEEDED limbs.  */
 /*unsigned int *mrz_realloc_if(mpz_t z,int n) {
@@ -363,7 +401,7 @@ mpz_sgn (const mpz_t u)
 mpz_swap (mpz_t u, mpz_t v)
 {
   int_swap (u->_mp_alloc, v->_mp_alloc);
-  unsigned int *_swap(u->_mp_d, v->_mp_d);
+  mp_ptr_swap(u->_mp_d, v->_mp_d);
   int_swap (u->_mp_size, v->_mp_size);
 }*/
 
diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h
index 2c952b8..1a6c313 100755
--- a/projects/mini-gmp.h
+++ b/projects/mini-gmp.h
@@ -1,4 +1,16 @@
-typedef struct
+/*@ 
+  Extern Coq (Zabs : Z -> Z) 
+             (Zmax : Z -> Z -> Z)
+             (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion)
+             (mpd_store_Z_compact: Z -> Z -> Z -> Z -> Assertion)
+             (mpd_store_list : Z -> list Z -> Z -> Assertion)
+             (store_Z: Z -> Z -> Assertion)
+             (list_store_Z : list Z -> Z -> Prop)
+             (list_store_Z_compact: list Z -> Z -> Prop)
+             (last: list Z -> Z -> Z)
+*/
+
+typedef struct __mpz_struct
 {
   int _mp_alloc;		/* Number of *limbs* allocated and pointed
 				   to by the _mp_d field.  */
@@ -16,7 +28,14 @@ typedef const __mpz_struct *mpz_srcptr;
 /* BEGIN Given Functions */
 
 /* Swap functions. */
-void int_swap(int x, int y);
+void int_swap(int x, int y)
+/*@
+  Require
+    emp
+  Ensure
+    x == y@pre && y == x@pre
+*/
+;
 
 void mp_ptr_swap(unsigned int *x, unsigned int *y);
 
@@ -24,13 +43,37 @@ void mpz_srcptr_swap(mpz_srcptr x, mpz_srcptr y);
 
 /* Memory allocation functions. */
 static unsigned int *
-gmp_alloc_limbs (int size);
+gmp_alloc_limbs (int size)
+/*@
+  Require
+    size >= 0
+  Ensure
+    store_undef_uint_array(__return, size)
+*/;
 
 static unsigned int *
-gmp_realloc_limbs (unsigned int *old, int old_size, int size);
+gmp_realloc_limbs (unsigned int *old, int old_size, int size)
+/*@
+  With
+    len n
+  Require
+    old_size >= 0 && size >= old_size &&
+    mpd_store_Z_compact(old, n, len, old_size)
+  Ensure
+    mpd_store_Z_compact(__return, n, len, size)
+*/;
 
 static void
-gmp_free_limbs (unsigned int *old, int size);
+gmp_free_limbs (unsigned int *old, int size)
+/*@
+  With
+    n len
+  Require
+    mpd_store_Z_compact(old, n, len, size)
+  Ensure
+    emp
+*/
+;
 
 /* END Given Functions  */
 
@@ -46,7 +89,7 @@ unsigned int mpn_sub_1 (unsigned int *, unsigned int *, int, unsigned int);
 unsigned int mpn_sub_n (unsigned int *, unsigned int *, unsigned int *, int);
 unsigned int mpn_sub (unsigned int *, unsigned int *, int, unsigned int *, int);
 
-void mpz_clear (mpz_t);
+void mpz_clear (mpz_t r);
 
 int mpz_sgn (const mpz_t);
 
@@ -58,13 +101,3 @@ void mpz_sub (mpz_t, const mpz_t, const mpz_t);
 
 void mpz_set (mpz_t, const mpz_t);
 
-/*@ 
-  Extern Coq (Zabs : Z -> Z) 
-             (Zmax : Z -> Z -> Z)
-             (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion)
-             (mpd_store_Z_compact: Z -> Z -> Z -> Z -> Assertion)
-             (mpd_store_list : Z -> list Z -> Z -> Assertion)
-             (list_store_Z : list Z -> Z -> Prop)
-             (list_store_Z_compact: list Z -> Z -> Prop)
-             (last: list Z -> Z -> Z)
-*/
\ No newline at end of file
diff --git a/projects/uint_array.strategies b/projects/uint_array.strategies
old mode 100644
new mode 100755