diff --git a/examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_gen_1.v b/examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_gen_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..7f9b586713adf2d75c8c049f330af335696de75b
--- /dev/null
+++ b/examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_gen_1.v
@@ -0,0 +1,727 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+Require int.Abs.
+Require int.EuclideanDivision.
+Require real.Real.
+Require real.RealInfix.
+Require real.FromInt.
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+Parameter pow2: Z -> Z.
+
+Axiom Power_0 : ((pow2 0%Z) = 1%Z).
+
+Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
+  ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
+
+Axiom Power_1 : ((pow2 1%Z) = 2%Z).
+
+Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
+  ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
+
+Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
+
+Axiom pow2_0 : ((pow2 0%Z) = 1%Z).
+
+Axiom pow2_1 : ((pow2 1%Z) = 2%Z).
+
+Axiom pow2_2 : ((pow2 2%Z) = 4%Z).
+
+Axiom pow2_3 : ((pow2 3%Z) = 8%Z).
+
+Axiom pow2_4 : ((pow2 4%Z) = 16%Z).
+
+Axiom pow2_5 : ((pow2 5%Z) = 32%Z).
+
+Axiom pow2_6 : ((pow2 6%Z) = 64%Z).
+
+Axiom pow2_7 : ((pow2 7%Z) = 128%Z).
+
+Axiom pow2_8 : ((pow2 8%Z) = 256%Z).
+
+Axiom pow2_9 : ((pow2 9%Z) = 512%Z).
+
+Axiom pow2_10 : ((pow2 10%Z) = 1024%Z).
+
+Axiom pow2_11 : ((pow2 11%Z) = 2048%Z).
+
+Axiom pow2_12 : ((pow2 12%Z) = 4096%Z).
+
+Axiom pow2_13 : ((pow2 13%Z) = 8192%Z).
+
+Axiom pow2_14 : ((pow2 14%Z) = 16384%Z).
+
+Axiom pow2_15 : ((pow2 15%Z) = 32768%Z).
+
+Axiom pow2_16 : ((pow2 16%Z) = 65536%Z).
+
+Axiom pow2_17 : ((pow2 17%Z) = 131072%Z).
+
+Axiom pow2_18 : ((pow2 18%Z) = 262144%Z).
+
+Axiom pow2_19 : ((pow2 19%Z) = 524288%Z).
+
+Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z).
+
+Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z).
+
+Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z).
+
+Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z).
+
+Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z).
+
+Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z).
+
+Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z).
+
+Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z).
+
+Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z).
+
+Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z).
+
+Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z).
+
+Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z).
+
+Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z).
+
+Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z).
+
+Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z).
+
+Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z).
+
+Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z).
+
+Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z).
+
+Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z).
+
+Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z).
+
+Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z).
+
+Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z).
+
+Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z).
+
+Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z).
+
+Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z).
+
+Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z).
+
+Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z).
+
+Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z).
+
+Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z).
+
+Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z).
+
+Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z).
+
+Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z).
+
+Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z).
+
+Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z).
+
+Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z).
+
+Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z).
+
+Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z).
+
+Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z).
+
+Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z).
+
+Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z).
+
+Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z).
+
+Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z).
+
+Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
+
+Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
+
+Parameter pow21: Z -> R.
+
+Axiom Power_01 : ((pow21 0%Z) = 1%R).
+
+Axiom Power_s1 : forall (n:Z), (0%Z <= n)%Z ->
+  ((pow21 (n + 1%Z)%Z) = (2%R * (pow21 n))%R).
+
+Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z ->
+  ((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R).
+
+Axiom Power_s_all : forall (n:Z),
+  ((pow21 (n + 1%Z)%Z) = (2%R * (pow21 n))%R).
+
+Axiom Power_p_all : forall (n:Z),
+  ((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R).
+
+Axiom Power_1_2 : ((05 / 10)%R = (Rdiv 1%R 2%R)%R).
+
+Axiom Power_11 : ((pow21 1%Z) = 2%R).
+
+Axiom Power_neg1 : ((pow21 (-1%Z)%Z) = (05 / 10)%R).
+
+Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow21 n) = 0%R).
+
+Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z ->
+  ((pow21 (-n)%Z) = (Rdiv 1%R (pow21 n))%R).
+
+Axiom Power_non_null : forall (n:Z), ~ ((pow21 n) = 0%R).
+
+Axiom Power_neg : forall (n:Z), ((pow21 (-n)%Z) = (Rdiv 1%R (pow21 n))%R).
+
+Axiom Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z ->
+  ((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%R).
+
+Axiom Power_sum1 : forall (n:Z) (m:Z),
+  ((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%R).
+
+Axiom Pow2_int_real : forall (x:Z), (0%Z <= x)%Z ->
+  ((pow21 x) = (IZR (pow2 x))).
+
+Axiom size_positive : (1%Z < 32%Z)%Z.
+
+Parameter bv : Type.
+
+Parameter nth: bv -> Z -> bool.
+
+Parameter bvzero: bv.
+
+Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvzero
+  n) = false).
+
+Parameter bvone: bv.
+
+Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
+  n) = true).
+
+(* Why3 assumption *)
+Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).
+
+Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
+
+Parameter bw_and: bv -> bv -> bv.
+
+Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
+
+Parameter bw_or: bv -> bv -> bv.
+
+Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
+
+Parameter bw_xor: bv -> bv -> bv.
+
+Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
+
+Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
+  n) = (negb (nth v2 n))).
+
+Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
+  n)).
+
+Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
+  n) = (negb (nth v1 n))).
+
+Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
+  n)).
+
+Parameter bw_not: bv -> bv.
+
+Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) ->
+  ((nth (bw_not v) n) = (negb (nth v n))).
+
+Parameter lsr: bv -> Z -> bv.
+
+Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
+  ((n + s)%Z < 32%Z)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
+
+Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
+  (32%Z <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false).
+
+Parameter asr: bv -> Z -> bv.
+
+Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (asr b s)
+  n) = (nth b (n + s)%Z)))).
+
+Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (asr b s)
+  n) = (nth b (32%Z - 1%Z)%Z)))).
+
+Parameter lsl: bv -> Z -> bv.
+
+Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
+  n) = (nth b (n - s)%Z)))).
+
+Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
+  n) = false))).
+
+Parameter to_nat_sub: bv -> Z -> Z -> Z.
+
+Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
+  (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
+  i) = (to_nat_sub b (j - 1%Z)%Z i))).
+
+Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
+  (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
+  i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)).
+
+Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
+  ((to_nat_sub b j i) = 0%Z).
+
+Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\
+  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
+  (i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b
+  i 0%Z))).
+
+Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < 32%Z)%Z /\
+  (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b
+  k) = false)) -> ((to_nat_sub b j i) = 0%Z)).
+
+Axiom to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\
+  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
+  (i <= k)%Z) -> ((nth b k) = true)) -> ((to_nat_sub b j
+  i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
+
+Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z),
+  ((j < 32%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
+  (k <= j)%Z) -> ((nth b1 k) = (nth b2 k))) -> ((to_nat_sub b1 j
+  i) = (to_nat_sub b2 j i))).
+
+Parameter from_int: Z -> bv.
+
+Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
+  (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
+  (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int n) i) = false).
+
+Axiom nth_from_int_high_odd : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
+  (0%Z <= i)%Z) /\
+  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth (from_int n) i) = true).
+
+Axiom nth_from_int_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z) -> ((nth (from_int n) 0%Z) = false).
+
+Axiom nth_from_int_low_odd : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z)) -> ((nth (from_int n) 0%Z) = true).
+
+Axiom nth_from_int_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
+  ((nth (from_int 0%Z) i) = false).
+
+Parameter from_int2c: Z -> bv.
+
+Axiom nth_sign_positive : forall (n:Z), (0%Z <= n)%Z -> ((nth (from_int2c n)
+  (32%Z - 1%Z)%Z) = false).
+
+Axiom nth_sign_negative : forall (n:Z), (n < 0%Z)%Z -> ((nth (from_int2c n)
+  (32%Z - 1%Z)%Z) = true).
+
+Axiom nth_from_int2c_high_even : forall (n:Z) (i:Z),
+  (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = false).
+
+Axiom nth_from_int2c_high_odd : forall (n:Z) (i:Z),
+  (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = true).
+
+Axiom nth_from_int2c_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z) -> ((nth (from_int2c n) 0%Z) = false).
+
+Axiom nth_from_int2c_low_odd : forall (n:Z),
+  (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
+  0%Z) = true).
+
+Axiom nth_from_int2c_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
+  ((nth (from_int2c 0%Z) i) = false).
+
+Axiom nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z), ((0%Z <= k)%Z /\
+  (k < i)%Z) -> ((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x)
+  k)).
+
+Axiom size_positive1 : (1%Z < 64%Z)%Z.
+
+Parameter bv1 : Type.
+
+Parameter nth1: bv1 -> Z -> bool.
+
+Parameter bvzero1: bv1.
+
+Axiom Nth_zero1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
+  ((nth1 bvzero1 n) = false).
+
+Parameter bvone1: bv1.
+
+Axiom Nth_one1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
+  ((nth1 bvone1 n) = true).
+
+(* Why3 assumption *)
+Definition eq1(v1:bv1) (v2:bv1): Prop := forall (n:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((nth1 v1 n) = (nth1 v2 n)).
+
+Axiom extensionality1 : forall (v1:bv1) (v2:bv1), (eq1 v1 v2) -> (v1 = v2).
+
+Parameter bw_and1: bv1 -> bv1 -> bv1.
+
+Axiom Nth_bw_and1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((nth1 (bw_and1 v1 v2) n) = (andb (nth1 v1 n) (nth1 v2
+  n))).
+
+Parameter bw_or1: bv1 -> bv1 -> bv1.
+
+Axiom Nth_bw_or1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((nth1 (bw_or1 v1 v2) n) = (orb (nth1 v1 n) (nth1 v2 n))).
+
+Parameter bw_xor1: bv1 -> bv1 -> bv1.
+
+Axiom Nth_bw_xor1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((nth1 (bw_xor1 v1 v2) n) = (xorb (nth1 v1 n) (nth1 v2
+  n))).
+
+Axiom Nth_bw_xor_v1true1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) /\ ((nth1 v1 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
+  n) = (negb (nth1 v2 n))).
+
+Axiom Nth_bw_xor_v1false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) /\ ((nth1 v1 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
+  n) = (nth1 v2 n)).
+
+Axiom Nth_bw_xor_v2true1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) /\ ((nth1 v2 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
+  n) = (negb (nth1 v1 n))).
+
+Axiom Nth_bw_xor_v2false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) /\ ((nth1 v2 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
+  n) = (nth1 v1 n)).
+
+Parameter bw_not1: bv1 -> bv1.
+
+Axiom Nth_bw_not1 : forall (v:bv1) (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
+  ((nth1 (bw_not1 v) n) = (negb (nth1 v n))).
+
+Parameter lsr1: bv1 -> Z -> bv1.
+
+Axiom lsr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
+  ((n + s)%Z < 64%Z)%Z)) -> ((nth1 (lsr1 b s) n) = (nth1 b (n + s)%Z)).
+
+Axiom lsr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
+  (64%Z <= (n + s)%Z)%Z)) -> ((nth1 (lsr1 b s) n) = false).
+
+Parameter asr1: bv1 -> Z -> bv1.
+
+Axiom asr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 64%Z)%Z -> ((nth1 (asr1 b
+  s) n) = (nth1 b (n + s)%Z)))).
+
+Axiom asr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> ((64%Z <= (n + s)%Z)%Z -> ((nth1 (asr1 b
+  s) n) = (nth1 b (64%Z - 1%Z)%Z)))).
+
+Parameter lsl1: bv1 -> Z -> bv1.
+
+Axiom lsl_nth_high1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth1 (lsl1 b
+  s) n) = (nth1 b (n - s)%Z)))).
+
+Axiom lsl_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth1 (lsl1 b s)
+  n) = false))).
+
+Parameter to_nat_sub1: bv1 -> Z -> Z -> Z.
+
+Axiom to_nat_sub_zero1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
+  (i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = false) -> ((to_nat_sub1 b j
+  i) = (to_nat_sub1 b (j - 1%Z)%Z i))).
+
+Axiom to_nat_sub_one1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
+  (i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = true) -> ((to_nat_sub1 b j
+  i) = ((pow2 (j - i)%Z) + (to_nat_sub1 b (j - 1%Z)%Z i))%Z)).
+
+Axiom to_nat_sub_high1 : forall (b:bv1) (j:Z) (i:Z), (j < i)%Z ->
+  ((to_nat_sub1 b j i) = 0%Z).
+
+Axiom to_nat_of_zero21 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\
+  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
+  (i < k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j
+  0%Z) = (to_nat_sub1 b i 0%Z))).
+
+Axiom to_nat_of_zero1 : forall (b:bv1) (i:Z) (j:Z), ((j < 64%Z)%Z /\
+  (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth1 b
+  k) = false)) -> ((to_nat_sub1 b j i) = 0%Z)).
+
+Axiom to_nat_of_one1 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\
+  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
+  (i <= k)%Z) -> ((nth1 b k) = true)) -> ((to_nat_sub1 b j
+  i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
+
+Axiom to_nat_sub_footprint1 : forall (b1:bv1) (b2:bv1) (j:Z) (i:Z),
+  ((j < 64%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
+  (k <= j)%Z) -> ((nth1 b1 k) = (nth1 b2 k))) -> ((to_nat_sub1 b1 j
+  i) = (to_nat_sub1 b2 j i))).
+
+Parameter from_int1: Z -> bv1.
+
+Axiom nth_from_int_high_even1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
+  (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
+  (pow2 i)) 2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = false).
+
+Axiom nth_from_int_high_odd1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
+  (0%Z <= i)%Z) /\
+  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = true).
+
+Axiom nth_from_int_low_even1 : forall (n:Z), ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z) -> ((nth1 (from_int1 n) 0%Z) = false).
+
+Axiom nth_from_int_low_odd1 : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z)) -> ((nth1 (from_int1 n) 0%Z) = true).
+
+Axiom nth_from_int_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
+  ((nth1 (from_int1 0%Z) i) = false).
+
+Parameter from_int2c1: Z -> bv1.
+
+Axiom nth_sign_positive1 : forall (n:Z), (0%Z <= n)%Z ->
+  ((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = false).
+
+Axiom nth_sign_negative1 : forall (n:Z), (n < 0%Z)%Z ->
+  ((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = true).
+
+Axiom nth_from_int2c_high_even1 : forall (n:Z) (i:Z),
+  (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) i) = false).
+
+Axiom nth_from_int2c_high_odd1 : forall (n:Z) (i:Z),
+  (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) i) = true).
+
+Axiom nth_from_int2c_low_even1 : forall (n:Z), ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z) -> ((nth1 (from_int2c1 n) 0%Z) = false).
+
+Axiom nth_from_int2c_low_odd1 : forall (n:Z),
+  (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n)
+  0%Z) = true).
+
+Axiom nth_from_int2c_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
+  ((nth1 (from_int2c1 0%Z) i) = false).
+
+Axiom nth_from_int2c_plus_pow21 : forall (x:Z) (k:Z) (i:Z), ((0%Z <= k)%Z /\
+  (k < i)%Z) -> ((nth1 (from_int2c1 (x + (pow2 i))%Z)
+  k) = (nth1 (from_int2c1 x) k)).
+
+Parameter concat: bv -> bv -> bv1.
+
+Axiom concat_low : forall (b1:bv) (b2:bv), forall (i:Z), ((0%Z <= i)%Z /\
+  (i < 32%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b2 i)).
+
+Axiom concat_high : forall (b1:bv) (b2:bv), forall (i:Z), ((32%Z <= i)%Z /\
+  (i < 64%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b1 (i - 32%Z)%Z)).
+
+Parameter double_of_bv64: bv1 -> R.
+
+Parameter sign_value: bool -> R.
+
+Axiom sign_value_false : ((sign_value false) = 1%R).
+
+Axiom sign_value_true : ((sign_value true) = (-1%R)%R).
+
+Axiom zero : forall (b:bv1), (((to_nat_sub1 b 62%Z 52%Z) = 0%Z) /\
+  ((to_nat_sub1 b 51%Z 0%Z) = 0%Z)) -> ((double_of_bv64 b) = 0%R).
+
+Axiom sign_of_double_positive : forall (b:bv1), ((nth1 b 63%Z) = false) ->
+  (0%R <= (double_of_bv64 b))%R.
+
+Axiom sign_of_double_negative : forall (b:bv1), ((nth1 b 63%Z) = true) ->
+  ((double_of_bv64 b) <= 0%R)%R.
+
+Axiom double_of_bv64_value : forall (b:bv1), ((0%Z < (to_nat_sub1 b 62%Z
+  52%Z))%Z /\ ((to_nat_sub1 b 62%Z 52%Z) < 2047%Z)%Z) ->
+  ((double_of_bv64 b) = (((sign_value (nth1 b 63%Z)) * (pow21 ((to_nat_sub1 b
+  62%Z 52%Z) - 1023%Z)%Z))%R * (1%R + ((IZR (to_nat_sub1 b 51%Z
+  0%Z)) * (pow21 (-52%Z)%Z))%R)%R)%R).
+
+Axiom jp0_30 : forall (i:Z), ((0%Z <= i)%Z /\ (i < 30%Z)%Z) ->
+  ((nth (from_int 2147483648%Z) i) = false).
+
+Axiom nth_const1 : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 30%Z)%Z) ->
+  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
+  i) = false).
+
+Axiom nth_const2 : ((nth1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 31%Z) = true).
+
+Axiom nth_const3 : forall (i:Z), ((32%Z <= i)%Z /\ (i <= 51%Z)%Z) ->
+  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
+  i) = false).
+
+Axiom nth_const4 : forall (i:Z), ((52%Z <= i)%Z /\ (i <= 53%Z)%Z) ->
+  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) i) = true).
+
+Axiom nth_const5 : forall (i:Z), ((54%Z <= i)%Z /\ (i <= 55%Z)%Z) ->
+  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
+  i) = false).
+
+Axiom nth_const6 : forall (i:Z), ((56%Z <= i)%Z /\ (i <= 57%Z)%Z) ->
+  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z)) i) = true).
+
+Axiom nth_const7 : forall (i:Z), ((58%Z <= i)%Z /\ (i <= 61%Z)%Z) ->
+  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
+  i) = false).
+
+Axiom nth_const8 : ((nth1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 62%Z) = true).
+
+Axiom nth_const9 : ((nth1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 63%Z) = false).
+
+Axiom sign_const : ((nth1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 63%Z) = false).
+
+Axiom exp_const : ((to_nat_sub1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 62%Z 52%Z) = 1075%Z).
+
+Axiom to_nat_mantissa_1 : ((to_nat_sub1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 30%Z 0%Z) = 0%Z).
+
+Axiom mantissa_const_nth2 : forall (i:Z), ((32%Z <= i)%Z /\ (i <= 51%Z)%Z) ->
+  ((nth1 (concat (from_int 1127219200%Z) (from_int 2147483648%Z))
+  i) = false).
+
+Axiom mantissa_const_to_nat51 : ((to_nat_sub1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 51%Z
+  0%Z) = (to_nat_sub1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 31%Z 0%Z)).
+
+Axiom mantissa_const : ((to_nat_sub1 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z)) 51%Z 0%Z) = (pow2 31%Z)).
+
+Axiom real1075m1023 : ((IZR (1075%Z - 1023%Z)%Z) = 52%R).
+
+Axiom real1075m1023_2 : ((1075%R - 1023%R)%R = 52%R).
+
+Axiom real52_a_m52 : ((((pow21 (1075%Z - 1023%Z)%Z) * (pow21 31%Z))%R * (pow21 (-52%Z)%Z))%R = (pow21 31%Z)).
+
+Axiom const_value0 : ((double_of_bv64 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z))) = ((1%R * (pow21 (1075%Z - 1023%Z)%Z))%R * (1%R + ((pow21 31%Z) * (pow21 (-52%Z)%Z))%R)%R)%R).
+
+Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z)
+  (from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R).
+
+(* Why3 assumption *)
+Definition jpxor(i:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c i)).
+
+(* Why3 assumption *)
+Definition var(i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)).
+
+(* Why3 assumption *)
+Definition var_as_double(x:Z): R := (double_of_bv64 (var x)).
+
+(* Why3 assumption *)
+Definition is_int32(x:Z): Prop := ((-(pow2 31%Z))%Z <= x)%Z /\
+  (x < (pow2 31%Z))%Z.
+
+Axiom nth_0_30 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
+  ((0%Z <= i)%Z /\ (i <= 30%Z)%Z)) -> ((nth (bw_xor (from_int 2147483648%Z)
+  (from_int2c x)) i) = (nth (from_int2c x) i)).
+
+Axiom nth_jpxor_0_30 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
+  ((0%Z <= i)%Z /\ (i <= 30%Z)%Z)) -> ((nth (jpxor x)
+  i) = (nth (from_int2c x) i)).
+
+Axiom nth_var31 : forall (x:Z), ((nth (jpxor x)
+  31%Z) = (negb (nth (from_int2c x) 31%Z))).
+
+Axiom to_nat_sub_0_30 : forall (x:Z), (is_int32 x) ->
+  ((to_nat_sub (bw_xor (from_int 2147483648%Z) (from_int2c x)) 30%Z
+  0%Z) = (to_nat_sub (from_int2c x) 30%Z 0%Z)).
+
+Axiom jpxorx_pos : forall (x:Z), (0%Z <= x)%Z ->
+  ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = true).
+
+Open Scope Z_scope.
+Require Import Why3.
+Ltac ae := why3 "alt-ergo" timelimit 3.
+
+(* Why3 goal *)
+Theorem from_int2c_to_nat_sub_gen : forall (i:Z), ((0%Z <= i)%Z /\
+  (i <= 30%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) ->
+  ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = x).
+intros i (h & h2).
+generalize h2; generalize h.
+pattern i; apply Z_lt_induction; auto.
+clear i h h2.
+intros i Hind Hi_pos Hi x Hx.
+assert (h:(i=0 \/ 0 < i)) by omega.
+destruct h.
+
+(* case i = 0 *)
+ae.
+
+(* case i > 0 *)
+
+assert (h:(0 <= x < pow2 (i-1) \/ 
+           pow2 (i-1) <= x < pow2 i)) by omega.
+destruct h.
+
+(* sub-case x0 < 2^(i0-1) *)
+rewrite to_nat_sub_zero; auto with zarith.
+apply nth_from_int2c_high_even; 
+   split; auto with zarith.
+rewrite EuclideanDivision.Div_inf; auto.
+
+(* sub-case 2^(i0-1) <= x0 < 2^i0*)
+rewrite to_nat_sub_one; auto with zarith.
+rewrite to_nat_sub_footprint with 
+  (b2 := (from_int2c (x - pow2 (i-1)))); auto with zarith.
+rewrite Hind; auto with zarith.
+ae.
+(*
+replace (i0 - 1 - 0) with (i0 -1) by omega; omega.
+*)
+ae.
+intros k Hk.
+replace x with (x - pow2 (i - 1) + pow2 (i - 1)) by omega.
+ae.
+rewrite nth_from_int2c_high_odd;auto.
+split.
+split;auto with zarith.
+rewrite Div_pow; auto with zarith.
+rewrite Mod_1y; omega.
+Qed.
+
+
diff --git a/examples/bitvectors/double_of_int/why3session.xml b/examples/bitvectors/double_of_int/why3session.xml
index 0078d09c40ae3271e01d4665551dd0075f9bf9da..8635d708f44ed87e14d13f58aac308797270d9fc 100644
--- a/examples/bitvectors/double_of_int/why3session.xml
+++ b/examples/bitvectors/double_of_int/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
 <why3session
- name="bitvectors/double_of_int/why3session.xml">
+ name="double_of_int/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -33,16 +33,16 @@
  <file
   name="../double_of_int.why"
   verified="false"
-  expanded="false">
+  expanded="true">
   <theory
    name="DoubleOfInt"
-   locfile="bitvectors/double_of_int/../double_of_int.why"
+   locfile="double_of_int/../double_of_int.why"
    loclnum="3" loccnumb="7" loccnume="18"
    verified="false"
    expanded="true">
    <goal
     name="jp0_30"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="25" loccnumb="8" loccnume="14"
     sum="dd1e1ceb3a9788e30e15fe9c25a9382a"
     proved="true"
@@ -59,7 +59,7 @@
    </goal>
    <goal
     name="nth_const1"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="41" loccnumb="8" loccnume="18"
     sum="261d6c248d650ec55f76dd63e84bc0e3"
     proved="true"
@@ -76,7 +76,7 @@
    </goal>
    <goal
     name="nth_const2"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="42" loccnumb="8" loccnume="18"
     sum="daf929e1d75bad068e4657175e1314a0"
     proved="true"
@@ -93,7 +93,7 @@
    </goal>
    <goal
     name="nth_const3"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="43" loccnumb="8" loccnume="18"
     sum="737f1a2db4422815ed1bc511f8080f23"
     proved="true"
@@ -110,7 +110,7 @@
    </goal>
    <goal
     name="nth_const4"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="44" loccnumb="8" loccnume="18"
     sum="182396c90f8ea54cff0a7541d27d6cec"
     proved="true"
@@ -127,7 +127,7 @@
    </goal>
    <goal
     name="nth_const5"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="45" loccnumb="8" loccnume="18"
     sum="1e5b09a5be939521831570ad2a468783"
     proved="true"
@@ -144,7 +144,7 @@
    </goal>
    <goal
     name="nth_const6"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="46" loccnumb="8" loccnume="18"
     sum="22d800cdc6cd6ab8b99dd99bd0b50323"
     proved="true"
@@ -161,7 +161,7 @@
    </goal>
    <goal
     name="nth_const7"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="47" loccnumb="8" loccnume="18"
     sum="f996be957be7f520983d69ddec7a44ef"
     proved="true"
@@ -178,7 +178,7 @@
    </goal>
    <goal
     name="nth_const8"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="48" loccnumb="8" loccnume="18"
     sum="4c23639c5ec039a10e6e325b1301e497"
     proved="true"
@@ -195,7 +195,7 @@
    </goal>
    <goal
     name="nth_const9"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="49" loccnumb="8" loccnume="18"
     sum="f76d9a803bc45a893cca15ce1d3335e8"
     proved="true"
@@ -212,7 +212,7 @@
    </goal>
    <goal
     name="sign_const"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="51" loccnumb="8" loccnume="18"
     sum="e7060da582f6a712f7fd94be17f80dd0"
     proved="true"
@@ -269,7 +269,7 @@
    </goal>
    <goal
     name="exp_const"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="53" loccnumb="8" loccnume="17"
     sum="5c5372a8718de21456f67bd1ca4d0307"
     proved="true"
@@ -287,7 +287,7 @@
    </goal>
    <goal
     name="to_nat_mantissa_1"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="55" loccnumb="8" loccnume="25"
     sum="1fa1973374d4d12946d36e021270b22f"
     proved="true"
@@ -320,7 +320,7 @@
    </goal>
    <goal
     name="mantissa_const_nth2"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="57" loccnumb="8" loccnume="27"
     sum="7433d00332d59717c1ffdf7ec45114f3"
     proved="true"
@@ -369,7 +369,7 @@
    </goal>
    <goal
     name="mantissa_const_to_nat51"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="60" loccnumb="8" loccnume="31"
     sum="50e2e6714169744021a05e4814b9dc09"
     proved="true"
@@ -402,7 +402,7 @@
    </goal>
    <goal
     name="mantissa_const"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="63" loccnumb="8" loccnume="22"
     sum="2ff85bcb325502fbe7940125d2f49870"
     proved="true"
@@ -435,7 +435,7 @@
    </goal>
    <goal
     name="real1075m1023"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="65" loccnumb="8" loccnume="21"
     sum="a8ea52f2a5b6aeabdde75cd427b9b403"
     proved="true"
@@ -484,7 +484,7 @@
    </goal>
    <goal
     name="real1075m1023_2"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="67" loccnumb="8" loccnume="23"
     sum="ef4f676fc3549cdde4e75e5d1a3bca21"
     proved="true"
@@ -541,48 +541,24 @@
    </goal>
    <goal
     name="real52_a_m52"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="69" loccnumb="8" loccnume="20"
     sum="091e7b7b8d42964e6fc2897ac38606c8"
-    proved="false"
-    expanded="true"
+    proved="true"
+    expanded="false"
     shape="ainfix =ainfix *.ainfix *.apow2ainfix -c1075c1023apow2c31apow2aprefix -c52apow2c31">
-    <proof
-     prover="5"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.12"/>
-    </proof>
     <proof
      prover="0"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.02"/>
-    </proof>
-    <proof
-     prover="4"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="unknown" time="0.00"/>
-    </proof>
-    <proof
-     prover="6"
-     timelimit="5"
+     timelimit="30"
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="5.01"/>
+     <result status="valid" time="11.12"/>
     </proof>
    </goal>
    <goal
     name="const_value0"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="71" loccnumb="8" loccnume="20"
     sum="053e10e406e6f3b38b72aece1d2ea1cc"
     proved="true"
@@ -615,7 +591,7 @@
    </goal>
    <goal
     name="const_value"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="74" loccnumb="8" loccnume="19"
     sum="15c0e266eaa7e83629a4b99a8c7fbbbc"
     proved="true"
@@ -656,7 +632,7 @@
    </goal>
    <goal
     name="nth_0_30"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="100" loccnumb="8" loccnume="16"
     sum="0f62d85765410f7e4511d07bde414f6b"
     proved="true"
@@ -689,7 +665,7 @@
    </goal>
    <goal
     name="nth_jpxor_0_30"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="102" loccnumb="8" loccnume="22"
     sum="122538c45d56e139bb3836e5a0df1b67"
     proved="true"
@@ -722,7 +698,7 @@
    </goal>
    <goal
     name="nth_var31"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="104" loccnumb="8" loccnume="17"
     sum="615ab90161692c1aeedf9d5b18404b7b"
     proved="true"
@@ -739,7 +715,7 @@
    </goal>
    <goal
     name="to_nat_sub_0_30"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="107" loccnumb="8" loccnume="23"
     sum="dfb01a9181d5c0966a7d6ec96d5ac09b"
     proved="true"
@@ -780,7 +756,7 @@
    </goal>
    <goal
     name="jpxorx_pos"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="114" loccnumb="8" loccnume="18"
     sum="44892484235e0bcc9ae0ae2692013aa4"
     proved="true"
@@ -829,7 +805,7 @@
    </goal>
    <goal
     name="from_int2c_to_nat_sub_gen"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="121" loccnumb="8" loccnume="33"
     sum="5ebb2305fcfec2d2956b80a9e1b8fb25"
     proved="false"
@@ -859,10 +835,19 @@
      archived="false">
      <result status="timeout" time="5.02"/>
     </proof>
+    <proof
+     prover="3"
+     timelimit="30"
+     memlimit="1000"
+     edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_gen_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="unknown" time="1.82"/>
+    </proof>
    </goal>
    <goal
     name="from_int2c_to_nat_sub"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="126" loccnumb="8" loccnume="29"
     sum="ad558127c1887d36861533f052fa7881"
     proved="false"
@@ -870,32 +855,48 @@
     shape="ainfix =ato_nat_subafrom_int2cV0c30c0V0Iainfix &gt;=V0c0Aais_int32V0F">
     <proof
      prover="5"
-     timelimit="5"
+     timelimit="30"
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="5.12"/>
+     <result status="highfailure" time="13.35"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="30"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="highfailure" time="0.19"/>
     </proof>
     <proof
      prover="0"
-     timelimit="5"
+     timelimit="30"
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="5.02"/>
+     <result status="timeout" time="30.10"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="30"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="highfailure" time="0.42"/>
     </proof>
     <proof
      prover="6"
-     timelimit="5"
+     timelimit="30"
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="5.02"/>
+     <result status="highfailure" time="17.06"/>
     </proof>
    </goal>
    <goal
     name="lemma1_pos"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="129" loccnumb="8" loccnume="18"
     sum="d139a96e73e962725d19413c55cb8b14"
     proved="false"
@@ -928,7 +929,7 @@
    </goal>
    <goal
     name="to_nat_sub_0_30_neg"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="133" loccnumb="8" loccnume="27"
     sum="99070120f3f44a6f210fea6e47536165"
     proved="true"
@@ -977,7 +978,7 @@
    </goal>
    <goal
     name="to_nat_sub_0_30_neg1"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="136" loccnumb="8" loccnume="28"
     sum="7700539e32b8c609dda46df0274b2fa4"
     proved="false"
@@ -1010,40 +1011,24 @@
    </goal>
    <goal
     name="lemma1_neg"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="139" loccnumb="8" loccnume="18"
     sum="f9b7369b8893d642cfe764d5817e2a95"
-    proved="false"
-    expanded="true"
+    proved="true"
+    expanded="false"
     shape="ainfix =ato_nat_subajpxorV0c31c0ainfix +apow2c31V0Iainfix &lt;V0c0Aais_int32V0F">
-    <proof
-     prover="5"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.12"/>
-    </proof>
-    <proof
-     prover="0"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.02"/>
-    </proof>
     <proof
      prover="6"
-     timelimit="5"
+     timelimit="30"
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="5.02"/>
+     <result status="valid" time="17.02"/>
     </proof>
    </goal>
    <goal
     name="lemma1"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="143" loccnumb="8" loccnume="14"
     sum="e5436643ae8166e1886bbfc73bcef98e"
     proved="true"
@@ -1092,7 +1077,7 @@
    </goal>
    <goal
     name="nth_var_0_31"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="150" loccnumb="8" loccnume="20"
     sum="89c321c8a42d15054c94acbb315456b7"
     proved="true"
@@ -1109,7 +1094,7 @@
    </goal>
    <goal
     name="to_nat_bv32_bv64_aux"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="152" loccnumb="8" loccnume="28"
     sum="4f0805d04df63d971aea75ebaf9472c3"
     proved="false"
@@ -1142,7 +1127,7 @@
    </goal>
    <goal
     name="to_nat_bv32_bv64"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="153" loccnumb="8" loccnume="24"
     sum="699d61b4aa5062d1a5a873d176ff9791"
     proved="true"
@@ -1191,7 +1176,7 @@
    </goal>
    <goal
     name="to_nat_var_0_31"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="155" loccnumb="8" loccnume="23"
     sum="c729301c6a34e59ea9125d9a394679c3"
     proved="true"
@@ -1216,7 +1201,7 @@
    </goal>
    <goal
     name="nth_var32to63"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="157" loccnumb="8" loccnume="21"
     sum="c851b5f6673b91b4b06b5fd003398545"
     proved="true"
@@ -1233,7 +1218,7 @@
    </goal>
    <goal
     name="nth_var3"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="160" loccnumb="8" loccnume="16"
     sum="7003f9037a411fde4f723ff382153471"
     proved="false"
@@ -1266,7 +1251,7 @@
    </goal>
    <goal
     name="lemma2"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="162" loccnumb="8" loccnume="14"
     sum="a2ab954dcfb69d430e68e06f3bb5b7c4"
     proved="false"
@@ -1299,7 +1284,7 @@
    </goal>
    <goal
     name="nth_var4"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="168" loccnumb="8" loccnume="16"
     sum="ca60d399662644602dcdc5e7eb7b5c99"
     proved="false"
@@ -1332,7 +1317,7 @@
    </goal>
    <goal
     name="nth_var5"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="169" loccnumb="8" loccnume="16"
     sum="1311aceb05d56d608a31019c9b8fc853"
     proved="false"
@@ -1365,7 +1350,7 @@
    </goal>
    <goal
     name="nth_var6"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="170" loccnumb="8" loccnume="16"
     sum="62a990ea451884ad814dc65f26b68723"
     proved="false"
@@ -1398,7 +1383,7 @@
    </goal>
    <goal
     name="nth_var7"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="171" loccnumb="8" loccnume="16"
     sum="0ca87efa235ad32388d508d439a1c584"
     proved="false"
@@ -1431,7 +1416,7 @@
    </goal>
    <goal
     name="nth_var8"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="172" loccnumb="8" loccnume="16"
     sum="b2a9d5ef0bc70b71cecb8d1f853841e9"
     proved="true"
@@ -1480,7 +1465,7 @@
    </goal>
    <goal
     name="lemma3"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="174" loccnumb="8" loccnume="14"
     sum="f208cabda76433852818607ea179a12a"
     proved="false"
@@ -1513,7 +1498,7 @@
    </goal>
    <goal
     name="nth_var9"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="180" loccnumb="8" loccnume="16"
     sum="6d245a608bf087a71d770aabc57ab6a3"
     proved="true"
@@ -1562,7 +1547,7 @@
    </goal>
    <goal
     name="lemma4"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="182" loccnumb="7" loccnume="13"
     sum="3da9d8f0facffb85e67706d706c80091"
     proved="true"
@@ -1611,7 +1596,7 @@
    </goal>
    <goal
     name="sign_var"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="187" loccnumb="8" loccnume="16"
     sum="0bedea94a55a57793652b1504fa64d33"
     proved="true"
@@ -1660,7 +1645,7 @@
    </goal>
    <goal
     name="var_value0"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="189" loccnumb="8" loccnume="18"
     sum="1521fd264894011a23d1b2278b59ffab"
     proved="false"
@@ -1693,7 +1678,7 @@
    </goal>
    <goal
     name="from_int_sum"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="193" loccnumb="8" loccnume="20"
     sum="46a666929f72dc28fb96c181a8e8655e"
     proved="true"
@@ -1742,7 +1727,7 @@
    </goal>
    <goal
     name="var_value3"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="196" loccnumb="8" loccnume="18"
     sum="86e1f78d6de3c68bc3a64d0f56d0dd4b"
     proved="true"
@@ -1775,7 +1760,7 @@
    </goal>
    <goal
     name="distr_pow52"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="200" loccnumb="8" loccnume="19"
     sum="35def1fd35c6c69db383267035a0df43"
     proved="true"
@@ -1800,7 +1785,7 @@
    </goal>
    <goal
     name="var_value4"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="203" loccnumb="8" loccnume="18"
     sum="39871f6d1faf8e4facdbd72197b7d1c6"
     proved="true"
@@ -1825,7 +1810,7 @@
    </goal>
    <goal
     name="pow31"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="206" loccnumb="8" loccnume="13"
     sum="fed4a3dc41110c1d523b22fcb93d6fe9"
     proved="true"
@@ -1858,7 +1843,7 @@
    </goal>
    <goal
     name="lemma5"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="208" loccnumb="8" loccnume="14"
     sum="7ef0b7f50b8a860065caf4c996a86d86"
     proved="true"
@@ -1907,7 +1892,7 @@
    </goal>
    <goal
     name="MainResult"
-    locfile="bitvectors/double_of_int/../double_of_int.why"
+    locfile="double_of_int/../double_of_int.why"
     loclnum="218" loccnumb="8" loccnume="18"
     sum="020690a482e10223e824a954a80eca9a"
     proved="true"
diff --git a/tests/bitvector1/bitvector1_TestDoubleOfInt_from_int2c_to_nat_sub_gen_1.v b/tests/bitvector1/bitvector1_TestDoubleOfInt_from_int2c_to_nat_sub_gen_1.v
index 133e90bfdebc359ee31b06c3203f2422aad74b35..a23caa7605853600b87ac8802ae4069fe5a2fcb1 100644
--- a/tests/bitvector1/bitvector1_TestDoubleOfInt_from_int2c_to_nat_sub_gen_1.v
+++ b/tests/bitvector1/bitvector1_TestDoubleOfInt_from_int2c_to_nat_sub_gen_1.v
@@ -6,7 +6,10 @@ Require int.Int.
 Require int.Abs.
 Require int.EuclideanDivision.
 Require real.Real.
+Require real.RealInfix.
 Require real.FromInt.
+
+(* Why3 assumption *)
 Definition implb(x:bool) (y:bool): bool := match (x,
   y) with
   | (true, false) => false
@@ -15,7 +18,6 @@ Definition implb(x:bool) (y:bool): bool := match (x,
 
 Parameter pow2: Z -> Z.
 
-
 Axiom Power_0 : ((pow2 0%Z) = 1%Z).
 
 Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
@@ -156,165 +158,131 @@ Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
 
 Parameter bv : Type.
 
-Axiom size_positive : (1%Z <  32%Z)%Z.
+Axiom size_positive : (1%Z < 32%Z)%Z.
 
 Parameter nth: bv -> Z -> bool.
 
-
 Parameter bvzero: bv.
 
-
-Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n <  32%Z)%Z) ->
-  ((nth bvzero n) = false).
+Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvzero
+  n) = false).
 
 Parameter bvone: bv.
 
-
-Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n <  32%Z)%Z) -> ((nth bvone
+Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone
   n) = true).
 
+(* Why3 assumption *)
 Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).
+  (n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).
 
 Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
 
 Parameter bw_and: bv -> bv -> bv.
 
-
 Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
+  (n < 32%Z)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
 
 Parameter bw_or: bv -> bv -> bv.
 
-
 Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
+  (n < 32%Z)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
 
 Parameter bw_xor: bv -> bv -> bv.
 
-
 Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
+  (n < 32%Z)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
 
 Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
+  (n < 32%Z)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
   n) = (negb (nth v2 n))).
 
 Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2)
-  n) = (nth v2 n)).
+  (n < 32%Z)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2
+  n)).
 
 Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
+  (n < 32%Z)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
   n) = (negb (nth v1 n))).
 
 Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2)
-  n) = (nth v1 n)).
+  (n < 32%Z)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1
+  n)).
 
 Parameter bw_not: bv -> bv.
 
-
-Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n <  32%Z)%Z) ->
+Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) ->
   ((nth (bw_not v) n) = (negb (nth v n))).
 
 Parameter lsr: bv -> Z -> bv.
 
-
 Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s <  32%Z)%Z) /\
-  ((n + s)%Z <  32%Z)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
+  (n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
+  ((n + s)%Z < 32%Z)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
 
 Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s <  32%Z)%Z) /\
+  (n < 32%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 32%Z)%Z) /\
   (32%Z <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false).
 
 Parameter asr: bv -> Z -> bv.
 
-
 Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z <  32%Z)%Z -> ((nth (asr b
-  s) n) = (nth b (n + s)%Z)))).
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (asr b s)
+  n) = (nth b (n + s)%Z)))).
 
 Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (asr b
-  s) n) = (nth b (32%Z - 1%Z)%Z)))).
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (asr b s)
+  n) = (nth b (32%Z - 1%Z)%Z)))).
 
 Parameter lsl: bv -> Z -> bv.
 
-
 Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
   n) = (nth b (n - s)%Z)))).
 
 Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z <  0%Z)%Z -> ((nth (lsl b s)
+  (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
   n) = false))).
 
 Parameter to_nat_sub: bv -> Z -> Z -> Z.
 
-
 Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
-  (i <= j)%Z) /\ (j <  32%Z)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
+  (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j
   i) = (to_nat_sub b (j - 1%Z)%Z i))).
 
 Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\
-  (i <= j)%Z) /\ (j <  32%Z)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
+  (i <= j)%Z) /\ (j < 32%Z)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
   i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)).
 
-Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j <  i)%Z ->
+Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
   ((to_nat_sub b j i) = 0%Z).
 
-Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j <  32%Z)%Z /\
+Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\
   (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
-  (i <  k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j
-  0%Z) = (to_nat_sub b i 0%Z))).
+  (i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b
+  i 0%Z))).
 
-Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), (((j <  32%Z)%Z /\
-  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
-  (i <= k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j i) = 0%Z)).
+Axiom to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < 32%Z)%Z /\
+  (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b
+  k) = false)) -> ((to_nat_sub b j i) = 0%Z)).
 
-Axiom to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j <  32%Z)%Z /\
+Axiom to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < 32%Z)%Z /\
   (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
   (i <= k)%Z) -> ((nth b k) = true)) -> ((to_nat_sub b j
   i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
 
 Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z),
-  ((j <  32%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
+  ((j < 32%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
   (k <= j)%Z) -> ((nth b1 k) = (nth b2 k))) -> ((to_nat_sub b1 j
   i) = (to_nat_sub b2 j i))).
 
 Parameter from_int: Z -> bv.
 
-
-Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x <  y)%Z) ->
-  ((int.EuclideanDivision.div x y) = 0%Z).
-
-Axiom Div_inf_neg : forall (x:Z) (y:Z), ((0%Z <  x)%Z /\ (x <= y)%Z) ->
-  ((int.EuclideanDivision.div (-x)%Z y) = (-1%Z)%Z).
-
-Axiom Mod_0 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z
-  y) = 0%Z).
-
-Axiom Mod_1y : forall (y:Z), (1%Z <  y)%Z -> ((int.EuclideanDivision.mod1 1%Z
-  y) = 1%Z).
-
-Axiom Mod_neg1y : forall (y:Z), (1%Z <  y)%Z ->
-  ((int.EuclideanDivision.mod1 (-1%Z)%Z y) = 1%Z).
-
-Axiom Div_pow : forall (x:Z) (i:Z), ((0%Z <  i)%Z /\
-  (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x <  (pow2 i))%Z)) ->
-  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z).
-
-Axiom Div_pow2 : forall (x:Z) (i:Z), ((0%Z <  i)%Z /\
-  (((-(pow2 i))%Z <= x)%Z /\ (x <  (-(pow2 (i - 1%Z)%Z))%Z)%Z)) ->
-  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z).
-
-Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i <  32%Z)%Z /\
+Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
   (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
   (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int n) i) = false).
 
-Axiom nth_from_int_high_odd : forall (n:Z) (i:Z), (((i <  32%Z)%Z /\
+Axiom nth_from_int_high_odd : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\
   (0%Z <= i)%Z) /\
   ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
   2%Z) = 0%Z)) -> ((nth (from_int n) i) = true).
@@ -327,25 +295,24 @@ Axiom nth_from_int_low_odd : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
 
 Axiom pow2i : forall (i:Z), (0%Z <= i)%Z -> ~ ((pow2 i) = 0%Z).
 
-Axiom nth_from_int_0 : forall (i:Z), ((i <  32%Z)%Z /\ (0%Z <= i)%Z) ->
+Axiom nth_from_int_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
   ((nth (from_int 0%Z) i) = false).
 
 Parameter from_int2c: Z -> bv.
 
-
 Axiom nth_sign_positive : forall (n:Z), (0%Z <= n)%Z -> ((nth (from_int2c n)
   (32%Z - 1%Z)%Z) = false).
 
-Axiom nth_sign_negative : forall (n:Z), (n <  0%Z)%Z -> ((nth (from_int2c n)
+Axiom nth_sign_negative : forall (n:Z), (n < 0%Z)%Z -> ((nth (from_int2c n)
   (32%Z - 1%Z)%Z) = true).
 
 Axiom nth_from_int2c_high_even : forall (n:Z) (i:Z),
-  (((i <  (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
   ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
   2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = false).
 
 Axiom nth_from_int2c_high_odd : forall (n:Z) (i:Z),
-  (((i <  (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  (((i < (32%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
   ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
   2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = true).
 
@@ -356,154 +323,142 @@ Axiom nth_from_int2c_low_odd : forall (n:Z),
   (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
   0%Z) = true).
 
-Axiom nth_from_int2c_0 : forall (i:Z), ((i <  32%Z)%Z /\ (0%Z <= i)%Z) ->
+Axiom nth_from_int2c_0 : forall (i:Z), ((i < 32%Z)%Z /\ (0%Z <= i)%Z) ->
   ((nth (from_int2c 0%Z) i) = false).
 
 Axiom nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z), ((0%Z <= k)%Z /\
-  (k <  i)%Z) -> ((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x)
+  (k < i)%Z) -> ((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x)
   k)).
 
 Parameter bv1 : Type.
 
-Axiom size_positive1 : (1%Z <  64%Z)%Z.
+Axiom size_positive1 : (1%Z < 64%Z)%Z.
 
 Parameter nth1: bv1 -> Z -> bool.
 
-
 Parameter bvzero1: bv1.
 
-
-Axiom Nth_zero1 : forall (n:Z), ((0%Z <= n)%Z /\ (n <  64%Z)%Z) ->
+Axiom Nth_zero1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
   ((nth1 bvzero1 n) = false).
 
 Parameter bvone1: bv1.
 
-
-Axiom Nth_one1 : forall (n:Z), ((0%Z <= n)%Z /\ (n <  64%Z)%Z) ->
+Axiom Nth_one1 : forall (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
   ((nth1 bvone1 n) = true).
 
+(* Why3 assumption *)
 Definition eq1(v1:bv1) (v2:bv1): Prop := forall (n:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((nth1 v1 n) = (nth1 v2 n)).
+  (n < 64%Z)%Z) -> ((nth1 v1 n) = (nth1 v2 n)).
 
 Axiom extensionality1 : forall (v1:bv1) (v2:bv1), (eq1 v1 v2) -> (v1 = v2).
 
 Parameter bw_and1: bv1 -> bv1 -> bv1.
 
-
 Axiom Nth_bw_and1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((nth1 (bw_and1 v1 v2) n) = (andb (nth1 v1 n) (nth1 v2
+  (n < 64%Z)%Z) -> ((nth1 (bw_and1 v1 v2) n) = (andb (nth1 v1 n) (nth1 v2
   n))).
 
 Parameter bw_or1: bv1 -> bv1 -> bv1.
 
-
 Axiom Nth_bw_or1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((nth1 (bw_or1 v1 v2) n) = (orb (nth1 v1 n) (nth1 v2
-  n))).
+  (n < 64%Z)%Z) -> ((nth1 (bw_or1 v1 v2) n) = (orb (nth1 v1 n) (nth1 v2 n))).
 
 Parameter bw_xor1: bv1 -> bv1 -> bv1.
 
-
 Axiom Nth_bw_xor1 : forall (v1:bv1) (v2:bv1) (n:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((nth1 (bw_xor1 v1 v2) n) = (xorb (nth1 v1 n) (nth1 v2
+  (n < 64%Z)%Z) -> ((nth1 (bw_xor1 v1 v2) n) = (xorb (nth1 v1 n) (nth1 v2
   n))).
 
 Axiom Nth_bw_xor_v1true1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) /\ ((nth1 v1 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
+  (n < 64%Z)%Z) /\ ((nth1 v1 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
   n) = (negb (nth1 v2 n))).
 
 Axiom Nth_bw_xor_v1false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) /\ ((nth1 v1 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
+  (n < 64%Z)%Z) /\ ((nth1 v1 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
   n) = (nth1 v2 n)).
 
 Axiom Nth_bw_xor_v2true1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) /\ ((nth1 v2 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
+  (n < 64%Z)%Z) /\ ((nth1 v2 n) = true)) -> ((nth1 (bw_xor1 v1 v2)
   n) = (negb (nth1 v1 n))).
 
 Axiom Nth_bw_xor_v2false1 : forall (v1:bv1) (v2:bv1) (n:Z), (((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) /\ ((nth1 v2 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
+  (n < 64%Z)%Z) /\ ((nth1 v2 n) = false)) -> ((nth1 (bw_xor1 v1 v2)
   n) = (nth1 v1 n)).
 
 Parameter bw_not1: bv1 -> bv1.
 
-
-Axiom Nth_bw_not1 : forall (v:bv1) (n:Z), ((0%Z <= n)%Z /\ (n <  64%Z)%Z) ->
+Axiom Nth_bw_not1 : forall (v:bv1) (n:Z), ((0%Z <= n)%Z /\ (n < 64%Z)%Z) ->
   ((nth1 (bw_not1 v) n) = (negb (nth1 v n))).
 
 Parameter lsr1: bv1 -> Z -> bv1.
 
-
 Axiom lsr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s <  64%Z)%Z) /\
-  ((n + s)%Z <  64%Z)%Z)) -> ((nth1 (lsr1 b s) n) = (nth1 b (n + s)%Z)).
+  (n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
+  ((n + s)%Z < 64%Z)%Z)) -> ((nth1 (lsr1 b s) n) = (nth1 b (n + s)%Z)).
 
 Axiom lsr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), (((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s <  64%Z)%Z) /\
+  (n < 64%Z)%Z) /\ (((0%Z <= s)%Z /\ (s < 64%Z)%Z) /\
   (64%Z <= (n + s)%Z)%Z)) -> ((nth1 (lsr1 b s) n) = false).
 
 Parameter asr1: bv1 -> Z -> bv1.
 
-
 Axiom asr_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z <  64%Z)%Z -> ((nth1 (asr1 b
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 64%Z)%Z -> ((nth1 (asr1 b
   s) n) = (nth1 b (n + s)%Z)))).
 
 Axiom asr_nth_high1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((0%Z <= s)%Z -> ((64%Z <= (n + s)%Z)%Z -> ((nth1 (asr1 b
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> ((64%Z <= (n + s)%Z)%Z -> ((nth1 (asr1 b
   s) n) = (nth1 b (64%Z - 1%Z)%Z)))).
 
 Parameter lsl1: bv1 -> Z -> bv1.
 
-
 Axiom lsl_nth_high1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth1 (lsl1 b
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth1 (lsl1 b
   s) n) = (nth1 b (n - s)%Z)))).
 
 Axiom lsl_nth_low1 : forall (b:bv1) (n:Z) (s:Z), ((0%Z <= n)%Z /\
-  (n <  64%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z <  0%Z)%Z -> ((nth1 (lsl1 b
-  s) n) = false))).
+  (n < 64%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth1 (lsl1 b s)
+  n) = false))).
 
 Parameter to_nat_sub1: bv1 -> Z -> Z -> Z.
 
-
 Axiom to_nat_sub_zero1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
-  (i <= j)%Z) /\ (j <  64%Z)%Z) -> (((nth1 b j) = false) -> ((to_nat_sub1 b j
+  (i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = false) -> ((to_nat_sub1 b j
   i) = (to_nat_sub1 b (j - 1%Z)%Z i))).
 
 Axiom to_nat_sub_one1 : forall (b:bv1) (j:Z) (i:Z), (((0%Z <= i)%Z /\
-  (i <= j)%Z) /\ (j <  64%Z)%Z) -> (((nth1 b j) = true) -> ((to_nat_sub1 b j
+  (i <= j)%Z) /\ (j < 64%Z)%Z) -> (((nth1 b j) = true) -> ((to_nat_sub1 b j
   i) = ((pow2 (j - i)%Z) + (to_nat_sub1 b (j - 1%Z)%Z i))%Z)).
 
-Axiom to_nat_sub_high1 : forall (b:bv1) (j:Z) (i:Z), (j <  i)%Z ->
+Axiom to_nat_sub_high1 : forall (b:bv1) (j:Z) (i:Z), (j < i)%Z ->
   ((to_nat_sub1 b j i) = 0%Z).
 
-Axiom to_nat_of_zero21 : forall (b:bv1) (i:Z) (j:Z), (((j <  64%Z)%Z /\
+Axiom to_nat_of_zero21 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\
   (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
-  (i <  k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j
+  (i < k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j
   0%Z) = (to_nat_sub1 b i 0%Z))).
 
-Axiom to_nat_of_zero1 : forall (b:bv1) (i:Z) (j:Z), (((j <  64%Z)%Z /\
-  (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
-  (i <= k)%Z) -> ((nth1 b k) = false)) -> ((to_nat_sub1 b j i) = 0%Z)).
+Axiom to_nat_of_zero1 : forall (b:bv1) (i:Z) (j:Z), ((j < 64%Z)%Z /\
+  (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth1 b
+  k) = false)) -> ((to_nat_sub1 b j i) = 0%Z)).
 
-Axiom to_nat_of_one1 : forall (b:bv1) (i:Z) (j:Z), (((j <  64%Z)%Z /\
+Axiom to_nat_of_one1 : forall (b:bv1) (i:Z) (j:Z), (((j < 64%Z)%Z /\
   (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\
   (i <= k)%Z) -> ((nth1 b k) = true)) -> ((to_nat_sub1 b j
   i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
 
 Axiom to_nat_sub_footprint1 : forall (b1:bv1) (b2:bv1) (j:Z) (i:Z),
-  ((j <  64%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
+  ((j < 64%Z)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((i <= k)%Z /\
   (k <= j)%Z) -> ((nth1 b1 k) = (nth1 b2 k))) -> ((to_nat_sub1 b1 j
   i) = (to_nat_sub1 b2 j i))).
 
 Parameter from_int1: Z -> bv1.
 
-
-Axiom nth_from_int_high_even1 : forall (n:Z) (i:Z), (((i <  64%Z)%Z /\
+Axiom nth_from_int_high_even1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
   (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
   (pow2 i)) 2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = false).
 
-Axiom nth_from_int_high_odd1 : forall (n:Z) (i:Z), (((i <  64%Z)%Z /\
+Axiom nth_from_int_high_odd1 : forall (n:Z) (i:Z), (((i < 64%Z)%Z /\
   (0%Z <= i)%Z) /\
   ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
   2%Z) = 0%Z)) -> ((nth1 (from_int1 n) i) = true).
@@ -516,25 +471,24 @@ Axiom nth_from_int_low_odd1 : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
 
 Axiom pow2i1 : forall (i:Z), (0%Z <= i)%Z -> ~ ((pow2 i) = 0%Z).
 
-Axiom nth_from_int_01 : forall (i:Z), ((i <  64%Z)%Z /\ (0%Z <= i)%Z) ->
+Axiom nth_from_int_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
   ((nth1 (from_int1 0%Z) i) = false).
 
 Parameter from_int2c1: Z -> bv1.
 
-
 Axiom nth_sign_positive1 : forall (n:Z), (0%Z <= n)%Z ->
   ((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = false).
 
-Axiom nth_sign_negative1 : forall (n:Z), (n <  0%Z)%Z ->
+Axiom nth_sign_negative1 : forall (n:Z), (n < 0%Z)%Z ->
   ((nth1 (from_int2c1 n) (64%Z - 1%Z)%Z) = true).
 
 Axiom nth_from_int2c_high_even1 : forall (n:Z) (i:Z),
-  (((i <  (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
   ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
   2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) i) = false).
 
 Axiom nth_from_int2c_high_odd1 : forall (n:Z) (i:Z),
-  (((i <  (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
+  (((i < (64%Z - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
   ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
   2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n) i) = true).
 
@@ -545,25 +499,23 @@ Axiom nth_from_int2c_low_odd1 : forall (n:Z),
   (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth1 (from_int2c1 n)
   0%Z) = true).
 
-Axiom nth_from_int2c_01 : forall (i:Z), ((i <  64%Z)%Z /\ (0%Z <= i)%Z) ->
+Axiom nth_from_int2c_01 : forall (i:Z), ((i < 64%Z)%Z /\ (0%Z <= i)%Z) ->
   ((nth1 (from_int2c1 0%Z) i) = false).
 
 Axiom nth_from_int2c_plus_pow21 : forall (x:Z) (k:Z) (i:Z), ((0%Z <= k)%Z /\
-  (k <  i)%Z) -> ((nth1 (from_int2c1 (x + (pow2 i))%Z)
+  (k < i)%Z) -> ((nth1 (from_int2c1 (x + (pow2 i))%Z)
   k) = (nth1 (from_int2c1 x) k)).
 
 Parameter concat: bv -> bv -> bv1.
 
-
 Axiom concat_low : forall (b1:bv) (b2:bv), forall (i:Z), ((0%Z <= i)%Z /\
-  (i <  32%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b2 i)).
+  (i < 32%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b2 i)).
 
 Axiom concat_high : forall (b1:bv) (b2:bv), forall (i:Z), ((32%Z <= i)%Z /\
-  (i <  64%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b1 (i - 32%Z)%Z)).
+  (i < 64%Z)%Z) -> ((nth1 (concat b1 b2) i) = (nth b1 (i - 32%Z)%Z)).
 
 Parameter pow21: Z -> R.
 
-
 Axiom Power_01 : ((pow21 0%Z) = 1%R).
 
 Axiom Power_s1 : forall (n:Z), (0%Z <= n)%Z ->
@@ -604,10 +556,8 @@ Axiom Pow2_int_real : forall (x:Z), (0%Z <= x)%Z ->
 
 Parameter double_of_bv64: bv1 -> R.
 
-
 Parameter sign_value: bool -> R.
 
-
 Axiom sign_value_false : ((sign_value false) = 1%R).
 
 Axiom sign_value_true : ((sign_value true) = (-1%R)%R).
@@ -621,13 +571,13 @@ Axiom sign_of_double_positive : forall (b:bv1), ((nth1 b 63%Z) = false) ->
 Axiom sign_of_double_negative : forall (b:bv1), ((nth1 b 63%Z) = true) ->
   ((double_of_bv64 b) <= 0%R)%R.
 
-Axiom double_of_bv64_value : forall (b:bv1), ((0%Z <  (to_nat_sub1 b 62%Z
-  52%Z))%Z /\ ((to_nat_sub1 b 62%Z 52%Z) <  2047%Z)%Z) ->
+Axiom double_of_bv64_value : forall (b:bv1), ((0%Z < (to_nat_sub1 b 62%Z
+  52%Z))%Z /\ ((to_nat_sub1 b 62%Z 52%Z) < 2047%Z)%Z) ->
   ((double_of_bv64 b) = (((sign_value (nth1 b 63%Z)) * (pow21 ((to_nat_sub1 b
   62%Z 52%Z) - 1023%Z)%Z))%R * (1%R + ((IZR (to_nat_sub1 b 51%Z
   0%Z)) * (pow21 (-52%Z)%Z))%R)%R)%R).
 
-Axiom jp0_30 : forall (i:Z), ((0%Z <= i)%Z /\ (i <  30%Z)%Z) ->
+Axiom jp0_30 : forall (i:Z), ((0%Z <= i)%Z /\ (i < 30%Z)%Z) ->
   ((nth (from_int 2147483648%Z) i) = false).
 
 Axiom nth_const1 : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 30%Z)%Z) ->
@@ -694,14 +644,18 @@ Axiom const_value0 : ((double_of_bv64 (concat (from_int 1127219200%Z)
 Axiom const_value : ((double_of_bv64 (concat (from_int 1127219200%Z)
   (from_int 2147483648%Z))) = ((pow21 52%Z) + (pow21 31%Z))%R).
 
+(* Why3 assumption *)
 Definition jpxor(i:Z): bv := (bw_xor (from_int 2147483648%Z) (from_int2c i)).
 
+(* Why3 assumption *)
 Definition var(i:Z): bv1 := (concat (from_int 1127219200%Z) (jpxor i)).
 
+(* Why3 assumption *)
 Definition var_as_double(x:Z): R := (double_of_bv64 (var x)).
 
+(* Why3 assumption *)
 Definition is_int32(x:Z): Prop := ((-(pow2 31%Z))%Z <= x)%Z /\
-  (x <  (pow2 31%Z))%Z.
+  (x < (pow2 31%Z))%Z.
 
 Axiom nth_0_30 : forall (x:Z), forall (i:Z), ((is_int32 x) /\
   ((0%Z <= i)%Z /\ (i <= 30%Z)%Z)) -> ((nth (bw_xor (from_int 2147483648%Z)
@@ -721,26 +675,17 @@ Axiom to_nat_sub_0_30 : forall (x:Z), (is_int32 x) ->
 Axiom jpxorx_pos : forall (x:Z), (0%Z <= x)%Z ->
   ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = true).
 
-Axiom jpxorx_neg : forall (x:Z), (x <  0%Z)%Z ->
-  ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = false).
-
-(* YOU MAY EDIT THE CONTEXT BELOW *)
 Open Scope Z_scope.
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Theorem from_int2c_to_nat_sub_gen : forall (i:Z), ((0%Z <= i)%Z /\
-  (i <= 31%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x <  (pow2 i))%Z) ->
+  (i <= 30%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) ->
   ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = x).
 (* YOU MAY EDIT THE PROOF BELOW *)
 intros i H.
 generalize H.
 cut (0 <= i); auto with zarith.
-apply Z_lt_induction with
-  (P:= fun i => 0 <= i ->
-     0 <= i <= 31 -> 
-     forall x:Z, 0 <= x < pow2 i -> 
-     to_nat_sub (from_int2c x) (i-1) 0 = x);
-  auto with zarith.
+pattern i; apply Z_lt_induction; auto with zarith.
 intros i0 Hind Hi0_pos Hi0 x0 Hx0.
 assert (h:(i0=0 \/ 0 < i0)) by omega.
 destruct h.
@@ -769,7 +714,7 @@ destruct h.
 rewrite to_nat_sub_zero; auto with zarith.
 apply nth_from_int2c_high_even; 
    split; auto with zarith.
-rewrite Div_inf; auto.
+rewrite EuclideanDivision.Div_inf; auto.
 
 (* sub-case 2^(i0-1) <= x0 < 2^i0*)
 
@@ -798,6 +743,5 @@ split;auto with zarith.
 rewrite Div_pow;auto with zarith.
 rewrite Mod_1y;omega.
 Qed.
-(* DO NOT EDIT BELOW *)
 
 
diff --git a/tests/bitvector1/why3session.xml b/tests/bitvector1/why3session.xml
index c2435d1cc2cfb1b1017d6f125e5d203148444806..786f5df06845df2054aea5198a7b07571bae7bcb 100644
--- a/tests/bitvector1/why3session.xml
+++ b/tests/bitvector1/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
 <why3session
- name="../why3/tests/bitvector1/why3session.xml">
+ name="tests/bitvector1/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -21,21 +21,17 @@
  <prover
   id="4"
   name="Coq"
-  version="8.3pl2"/>
+  version="8.3pl4"/>
  <prover
   id="5"
-  name="Coq"
-  version="8.3pl3"/>
- <prover
-  id="6"
   name="Gappa"
   version="0.16.0"/>
  <prover
-  id="7"
+  id="6"
   name="Z3"
   version="2.19"/>
  <prover
-  id="8"
+  id="7"
   name="Z3"
   version="3.2"/>
  <file
@@ -44,20 +40,20 @@
   expanded="true">
   <theory
    name="Div"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="2" loccnumb="7" loccnume="10"
    verified="true"
    expanded="true">
   </theory>
   <theory
    name="Pow2int"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="14" loccnumb="7" loccnume="14"
    verified="true"
    expanded="false">
    <goal
     name="Power_1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="24" loccnumb="8" loccnume="15"
     sum="33bc32635e211600fb0149bbdc4cf0c0"
     proved="true"
@@ -74,7 +70,7 @@
    </goal>
    <goal
     name="Power_sum"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="26" loccnumb="8" loccnume="17"
     sum="01d41b81dadfb478ff33dc9bdb7d39d1"
     proved="true"
@@ -84,23 +80,23 @@
      prover="1"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="unknown" time="0.42"/>
+     <result status="unknown" time="0.44"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_Pow2int_Power_sum_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.92"/>
+     <result status="valid" time="0.51"/>
     </proof>
    </goal>
    <goal
     name="pow2_0"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="29" loccnumb="8" loccnume="14"
     sum="9794b272135f9083d883502006a81613"
     proved="true"
@@ -117,7 +113,7 @@
    </goal>
    <goal
     name="pow2_1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="30" loccnumb="8" loccnume="14"
     sum="8ea4ae29afe088d53b9759d50cbb882d"
     proved="true"
@@ -134,7 +130,7 @@
    </goal>
    <goal
     name="pow2_2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="31" loccnumb="8" loccnume="14"
     sum="35b01a76a770a4157a52f3c1ea44358c"
     proved="true"
@@ -151,7 +147,7 @@
    </goal>
    <goal
     name="pow2_3"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="32" loccnumb="8" loccnume="14"
     sum="3db6574d1e708d6137a8b68bca07add7"
     proved="true"
@@ -163,12 +159,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_4"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="33" loccnumb="8" loccnume="14"
     sum="5899844ea5662102656716c172083530"
     proved="true"
@@ -180,12 +176,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="pow2_5"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="34" loccnumb="8" loccnume="14"
     sum="123c05eece455b3dba4e97936010717e"
     proved="true"
@@ -197,12 +193,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_6"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="35" loccnumb="8" loccnume="14"
     sum="e41d124a89a9602924028523a09eec1c"
     proved="true"
@@ -219,7 +215,7 @@
    </goal>
    <goal
     name="pow2_7"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="36" loccnumb="8" loccnume="14"
     sum="a9ddc51c774adf8a74f2a159a12e7d72"
     proved="true"
@@ -231,12 +227,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_8"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="37" loccnumb="8" loccnume="14"
     sum="472399ebbb7ad2ab31aeadabf4f1c40b"
     proved="true"
@@ -253,7 +249,7 @@
    </goal>
    <goal
     name="pow2_9"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="38" loccnumb="8" loccnume="14"
     sum="509a8c58f5d388832ba585f63b129396"
     proved="true"
@@ -270,7 +266,7 @@
    </goal>
    <goal
     name="pow2_10"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="39" loccnumb="8" loccnume="15"
     sum="d6adeef30108ccf3ca8ff96cc79c0384"
     proved="true"
@@ -282,12 +278,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_11"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="40" loccnumb="8" loccnume="15"
     sum="2fc6934a7c65a6cf9f7385120200d3cc"
     proved="true"
@@ -299,12 +295,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_12"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="41" loccnumb="8" loccnume="15"
     sum="83b4da45905980037cbf27970a00d0f6"
     proved="true"
@@ -316,12 +312,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_13"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="42" loccnumb="8" loccnume="15"
     sum="0f0e7aa46846e876ad0cecf7a7e0ff1c"
     proved="true"
@@ -333,12 +329,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="pow2_14"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="43" loccnumb="8" loccnume="15"
     sum="e7c29541374bf9c94a7f532421e89694"
     proved="true"
@@ -355,7 +351,7 @@
    </goal>
    <goal
     name="pow2_15"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="44" loccnumb="8" loccnume="15"
     sum="094b5980d31b162d032b09386b18f360"
     proved="true"
@@ -372,7 +368,7 @@
    </goal>
    <goal
     name="pow2_16"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="45" loccnumb="8" loccnume="15"
     sum="ea51c4218ceaeb142fee6ff62106ae8f"
     proved="true"
@@ -384,12 +380,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_17"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="46" loccnumb="8" loccnume="15"
     sum="12a737879085e2e075b9d3e70ac33e04"
     proved="true"
@@ -406,7 +402,7 @@
    </goal>
    <goal
     name="pow2_18"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="47" loccnumb="8" loccnume="15"
     sum="290b228a2edc31070908c666cd3081df"
     proved="true"
@@ -418,12 +414,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_19"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="48" loccnumb="8" loccnume="15"
     sum="547a19693be161698849a89a6d148ed1"
     proved="true"
@@ -440,7 +436,7 @@
    </goal>
    <goal
     name="pow2_20"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="49" loccnumb="8" loccnume="15"
     sum="e1248f70278c0454eef86e8fb6a4f0d0"
     proved="true"
@@ -457,7 +453,7 @@
    </goal>
    <goal
     name="pow2_21"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="50" loccnumb="8" loccnume="15"
     sum="1d2b4283b1db05305d5a6b064bffe241"
     proved="true"
@@ -469,12 +465,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_22"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="51" loccnumb="8" loccnume="15"
     sum="8abe2ce42e2ef911d45a717b00e8424f"
     proved="true"
@@ -491,7 +487,7 @@
    </goal>
    <goal
     name="pow2_23"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="52" loccnumb="8" loccnume="15"
     sum="bdd8a1eb83a44b5d793efd215129956e"
     proved="true"
@@ -508,7 +504,7 @@
    </goal>
    <goal
     name="pow2_24"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="53" loccnumb="8" loccnume="15"
     sum="4990ce4c33a449a56d1dabcdbbb469fe"
     proved="true"
@@ -525,7 +521,7 @@
    </goal>
    <goal
     name="pow2_25"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="54" loccnumb="8" loccnume="15"
     sum="eb06671a314765ab02a4e9c53dc72ed1"
     proved="true"
@@ -542,7 +538,7 @@
    </goal>
    <goal
     name="pow2_26"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="55" loccnumb="8" loccnume="15"
     sum="d8858d06cafdf610fbb840adbc4e706b"
     proved="true"
@@ -559,7 +555,7 @@
    </goal>
    <goal
     name="pow2_27"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="56" loccnumb="8" loccnume="15"
     sum="bf665a0e14089c4d061e073a2d6c825d"
     proved="true"
@@ -571,12 +567,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_28"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="57" loccnumb="8" loccnume="15"
     sum="3940a6d01f55ae1b3c46548d4ad151e4"
     proved="true"
@@ -588,12 +584,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_29"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="58" loccnumb="8" loccnume="15"
     sum="7fac9909e0eafa383177de67c5e75220"
     proved="true"
@@ -610,7 +606,7 @@
    </goal>
    <goal
     name="pow2_30"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="59" loccnumb="8" loccnume="15"
     sum="ef293872f7cb7dfafecd26216bcf2e8b"
     proved="true"
@@ -622,12 +618,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_31"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="60" loccnumb="8" loccnume="15"
     sum="cb4b8e74bd1f9883fbfb5825c8120052"
     proved="true"
@@ -639,12 +635,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_32"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="61" loccnumb="8" loccnume="15"
     sum="7b9e3af148c9f88a4580180c03f545e0"
     proved="true"
@@ -661,7 +657,7 @@
    </goal>
    <goal
     name="pow2_33"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="62" loccnumb="8" loccnume="15"
     sum="0c6f09e705a4175d88fc0365f86d7a7a"
     proved="true"
@@ -678,7 +674,7 @@
    </goal>
    <goal
     name="pow2_34"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="63" loccnumb="8" loccnume="15"
     sum="0b042dc50bf0e7a680e389047d3b6390"
     proved="true"
@@ -690,12 +686,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_35"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="64" loccnumb="8" loccnume="15"
     sum="ae2727eb7ade2b9d139abc4ebc961268"
     proved="true"
@@ -707,12 +703,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_36"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="65" loccnumb="8" loccnume="15"
     sum="6ab27e9b63fe6411a03a743ed5965fde"
     proved="true"
@@ -724,12 +720,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_37"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="66" loccnumb="8" loccnume="15"
     sum="78ad5ad66e8af2da00bdb152b5e4e824"
     proved="true"
@@ -741,12 +737,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_38"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="67" loccnumb="8" loccnume="15"
     sum="276acf78adeb6b8d888de9fc764138b7"
     proved="true"
@@ -758,12 +754,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_39"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="68" loccnumb="8" loccnume="15"
     sum="14410890c7b738dfc513da7d8321a712"
     proved="true"
@@ -780,7 +776,7 @@
    </goal>
    <goal
     name="pow2_40"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="69" loccnumb="8" loccnume="15"
     sum="91476c76798188591b1ea5e5dfd93bc7"
     proved="true"
@@ -797,7 +793,7 @@
    </goal>
    <goal
     name="pow2_41"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="70" loccnumb="8" loccnume="15"
     sum="c660f3b73805182e6a37905eb7f28a52"
     proved="true"
@@ -809,12 +805,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_42"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="71" loccnumb="8" loccnume="15"
     sum="7cd369fcccf9b6a7b6c5e0953ff14d52"
     proved="true"
@@ -826,12 +822,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_43"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="72" loccnumb="8" loccnume="15"
     sum="a053f993447f03a2213e58e3e661c3b3"
     proved="true"
@@ -843,12 +839,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_44"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="73" loccnumb="8" loccnume="15"
     sum="3d7ce098e4b05822d7664786379b561b"
     proved="true"
@@ -865,7 +861,7 @@
    </goal>
    <goal
     name="pow2_45"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="74" loccnumb="8" loccnume="15"
     sum="d11513042064e38458afcdd745518fea"
     proved="true"
@@ -877,12 +873,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="pow2_46"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="75" loccnumb="8" loccnume="15"
     sum="71461f3d79ed1598d4dd25438d8d54d8"
     proved="true"
@@ -899,7 +895,7 @@
    </goal>
    <goal
     name="pow2_47"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="76" loccnumb="8" loccnume="15"
     sum="3b91e34a668cf1212e04d21377589a00"
     proved="true"
@@ -911,12 +907,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_48"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="77" loccnumb="8" loccnume="15"
     sum="c13dea3a7e10208ea33d571bb2801b4a"
     proved="true"
@@ -928,12 +924,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_49"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="78" loccnumb="8" loccnume="15"
     sum="b02fd2869282ab1c22255dc82156e658"
     proved="true"
@@ -950,7 +946,7 @@
    </goal>
    <goal
     name="pow2_50"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="79" loccnumb="8" loccnume="15"
     sum="12acc6953daaab058d1b876bd2772bf8"
     proved="true"
@@ -967,7 +963,7 @@
    </goal>
    <goal
     name="pow2_51"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="80" loccnumb="8" loccnume="15"
     sum="a022cca825c5af8c29fbb08e5172eca0"
     proved="true"
@@ -979,12 +975,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_52"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="81" loccnumb="8" loccnume="15"
     sum="e8de7e58bb46ffad0f357d106e917592"
     proved="true"
@@ -1001,7 +997,7 @@
    </goal>
    <goal
     name="pow2_53"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="82" loccnumb="8" loccnume="15"
     sum="87afc9b602efd47d35fbfbd13fd20bda"
     proved="true"
@@ -1018,7 +1014,7 @@
    </goal>
    <goal
     name="pow2_54"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="83" loccnumb="8" loccnume="15"
     sum="f37fc15a50c18db98edd105750fd8f60"
     proved="true"
@@ -1035,7 +1031,7 @@
    </goal>
    <goal
     name="pow2_55"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="84" loccnumb="8" loccnume="15"
     sum="08f56546a3020a6958c11504d455090c"
     proved="true"
@@ -1052,7 +1048,7 @@
    </goal>
    <goal
     name="pow2_56"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="85" loccnumb="8" loccnume="15"
     sum="710e72b621ada134e9fb7c5e6bb6f301"
     proved="true"
@@ -1064,12 +1060,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_57"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="86" loccnumb="8" loccnume="15"
     sum="5999c3dc482f71d7b7a2501f683a6963"
     proved="true"
@@ -1081,12 +1077,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_58"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="87" loccnumb="8" loccnume="15"
     sum="9f00971587c4b5fccf4317dc1fa87554"
     proved="true"
@@ -1098,12 +1094,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_59"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="88" loccnumb="8" loccnume="15"
     sum="51f4ed49f1ce278ae4ad90d15818e529"
     proved="true"
@@ -1115,12 +1111,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_60"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="89" loccnumb="8" loccnume="15"
     sum="16c186a2d2f9d6368793d86d9eaf0406"
     proved="true"
@@ -1132,12 +1128,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_61"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="90" loccnumb="8" loccnume="15"
     sum="bf7bf7a47369493c8f26fc375e2136e9"
     proved="true"
@@ -1154,7 +1150,7 @@
    </goal>
    <goal
     name="pow2_62"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="91" loccnumb="8" loccnume="15"
     sum="7f6273378ef33281b938ffeaa9b5f921"
     proved="true"
@@ -1166,12 +1162,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2_63"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="92" loccnumb="8" loccnume="15"
     sum="0e9efb9e5c8d9f985aaa6fa576c72e23"
     proved="true"
@@ -1183,26 +1179,26 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
   </theory>
   <theory
    name="Pow2real"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="96" loccnumb="7" loccnume="15"
    verified="true"
    expanded="false">
    <goal
     name="Power_s_all"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="106" loccnumb="8" loccnume="19"
     sum="6f696a9d2f07d6172a73d8dd30ac7b70"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix +V0c1ainfix *.c2.0apow2V0F">
     <proof
-     prover="7"
+     prover="6"
      timelimit="5"
      memlimit="0"
      obsolete="false"
@@ -1231,27 +1227,27 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="8"
+     prover="7"
      timelimit="5"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="Power_p_all"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="108" loccnumb="8" loccnume="19"
     sum="ede41bed7ccb894e2af4fcf008dbd14f"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix -V0c1ainfix *.c0.5apow2V0F">
     <proof
-     prover="7"
+     prover="6"
      timelimit="5"
      memlimit="0"
      obsolete="false"
@@ -1283,7 +1279,7 @@
      <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="8"
+     prover="7"
      timelimit="5"
      memlimit="0"
      obsolete="false"
@@ -1293,7 +1289,7 @@
    </goal>
    <goal
     name="Power_1_2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="110" loccnumb="8" loccnume="17"
     sum="84a753b158c26d8042cfabd64c4737e0"
     proved="true"
@@ -1310,7 +1306,7 @@
    </goal>
    <goal
     name="Power_1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="112" loccnumb="8" loccnume="15"
     sum="14d8bd428d2a57bb612ee84ae54e1aba"
     proved="true"
@@ -1327,7 +1323,7 @@
    </goal>
    <goal
     name="Power_neg1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="114" loccnumb="8" loccnume="18"
     sum="c7a57a300a9ae5d0db11a4a441d0e606"
     proved="true"
@@ -1339,66 +1335,66 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="Power_non_null_aux"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="116" loccnumb="8" loccnume="26"
     sum="742640b78c6f8972a42743290fdb56c5"
     proved="true"
     expanded="false"
     shape="ainfix =apow2V0c0.0NIainfix &gt;=V0c0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      edited="bitvector1_Pow2real_Power_non_null_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.24"/>
+     <result status="valid" time="0.75"/>
     </proof>
    </goal>
    <goal
     name="Power_neg_aux"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="118" loccnumb="8" loccnume="21"
     sum="2cbd515615e025e022da59b7fe3978d4"
     proved="true"
     expanded="false"
     shape="ainfix =apow2aprefix -V0ainfix /.c1.0apow2V0Iainfix &gt;=V0c0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      edited="bitvector1_Pow2real_Power_neg_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.91"/>
+     <result status="valid" time="0.56"/>
     </proof>
    </goal>
    <goal
     name="Power_non_null"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="120" loccnumb="8" loccnume="22"
     sum="e76a0e7bb90eb5890c701551fc6bc41c"
     proved="true"
     expanded="false"
     shape="ainfix =apow2V0c0.0NF">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      edited="bitvector1_Pow2real_Power_non_null_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.79"/>
+     <result status="valid" time="0.48"/>
     </proof>
    </goal>
    <goal
     name="Power_neg"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="122" loccnumb="8" loccnume="17"
     sum="c98172b037771dc004f33a01af8dc28b"
     proved="true"
@@ -1410,73 +1406,73 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="Power_sum_aux"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="124" loccnumb="8" loccnume="21"
     sum="f172c7e0f52f667bb7b9c8653216ef40"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix +V0V1ainfix *.apow2V0apow2V1Iainfix &gt;=V1c0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      edited="bitvector1_Pow2real_Power_sum_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.87"/>
+     <result status="valid" time="0.53"/>
     </proof>
    </goal>
    <goal
     name="Power_sum"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="126" loccnumb="8" loccnume="17"
     sum="763c6533a99370f6102384b6bb2768d3"
     proved="true"
     expanded="false"
     shape="ainfix =apow2ainfix +V0V1ainfix *.apow2V0apow2V1F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="2"
      memlimit="0"
      edited="bitvector1_Pow2real_Power_sum_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.81"/>
+     <result status="valid" time="0.52"/>
     </proof>
    </goal>
    <goal
     name="Pow2_int_real"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="131" loccnumb="8" loccnume="21"
     sum="514327c3c11c2e923c55fc4ee15c6412"
     proved="true"
     expanded="false"
     shape="ainfix =apow2V0afrom_intapow2V0Iainfix &gt;=V0c0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_Pow2real_Pow2_int_real_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.94"/>
+     <result status="valid" time="0.55"/>
     </proof>
    </goal>
   </theory>
   <theory
    name="BitVector"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="136" loccnumb="7" loccnume="16"
    verified="false"
-   expanded="false">
+   expanded="true">
    <goal
     name="Nth_bw_xor_v1true"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="179" loccnumb="8" loccnume="25"
     sum="f4055a08a84f47e363415170a6151518"
     proved="true"
@@ -1488,12 +1484,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.27"/>
+     <result status="valid" time="0.18"/>
     </proof>
    </goal>
    <goal
     name="Nth_bw_xor_v1false"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="183" loccnumb="8" loccnume="26"
     sum="151b6a96d134757456935199951d5b35"
     proved="true"
@@ -1503,31 +1499,31 @@
      prover="1"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="timeout" time="10.07"/>
+     <result status="timeout" time="10.06"/>
     </proof>
     <proof
      prover="2"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.00"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_BitVector_Nth_bw_xor_v1false_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.97"/>
+     <result status="valid" time="0.52"/>
     </proof>
    </goal>
    <goal
     name="Nth_bw_xor_v2true"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="187" loccnumb="8" loccnume="25"
     sum="bcb94308e26ad7d115475bf837d5fbd6"
     proved="true"
@@ -1539,12 +1535,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.05"/>
     </proof>
    </goal>
    <goal
     name="Nth_bw_xor_v2false"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="191" loccnumb="8" loccnume="26"
     sum="8301688caf57a855c158df910d3bd043"
     proved="true"
@@ -1556,96 +1552,96 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.27"/>
+     <result status="valid" time="0.18"/>
     </proof>
    </goal>
    <goal
     name="to_nat_of_zero2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="327" loccnumb="8" loccnume="23"
     sum="7f64543adc67ee57719721c9e3008adc"
     proved="true"
     expanded="false"
     shape="ainfix =ato_nat_subV0V2c0ato_nat_subV0V1c0Iainfix =anthV0V3aFalseIainfix &gt;V3V1Aainfix &gt;=V2V3FIainfix &gt;=V1c0Aainfix &gt;=V2V1Aainfix &gt;asizeV2F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_BitVector_to_nat_of_zero2_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.12"/>
+     <result status="valid" time="0.58"/>
     </proof>
    </goal>
    <goal
     name="to_nat_of_zero"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="333" loccnumb="8" loccnume="22"
     sum="7e4513c40ed4b921457bd4c09bf06a6b"
     proved="true"
     expanded="false"
     shape="ainfix =ato_nat_subV0V2V1c0Iainfix =anthV0V3aFalseIainfix &gt;=V3V1Aainfix &gt;=V2V3FIainfix &gt;=V1c0Aainfix &gt;asizeV2F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      edited="bitvector1_BitVector_to_nat_of_zero_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.98"/>
+     <result status="valid" time="0.58"/>
     </proof>
    </goal>
    <goal
     name="to_nat_of_one"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="338" loccnumb="8" loccnume="21"
     sum="767b48e07ed56de6b7f3db0ae6bfeac7"
     proved="true"
     expanded="false"
     shape="ainfix =ato_nat_subV0V2V1ainfix -apow2ainfix +ainfix -V2V1c1c1Iainfix =anthV0V3aTrueIainfix &gt;=V3V1Aainfix &gt;=V2V3FIainfix &gt;=V1c0Aainfix &gt;=V2V1Aainfix &gt;asizeV2F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_BitVector_to_nat_of_one_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.09"/>
+     <result status="valid" time="0.57"/>
     </proof>
    </goal>
    <goal
     name="to_nat_sub_footprint"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="343" loccnumb="8" loccnume="28"
     sum="0a8324dea32fba16bfe399439cb987b4"
     proved="true"
     expanded="false"
     shape="ainfix =ato_nat_subV0V2V3ato_nat_subV1V2V3Iainfix =anthV0V4anthV1V4Iainfix &lt;=V4V2Aainfix &lt;=V3V4FIainfix &gt;=V3c0Aainfix &gt;asizeV2F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="60"
      memlimit="0"
      edited="bitvector1_BitVector_to_nat_sub_footprint_3.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.31"/>
+     <result status="valid" time="0.70"/>
     </proof>
    </goal>
    <goal
     name="nth_from_int_low_even"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="430" loccnumb="8" loccnume="29"
     sum="983a963c8a4cd81390c5b1d977ffd618"
     proved="true"
     expanded="false"
     shape="ainfix =anthafrom_intV0c0aFalseIainfix =amodV0c2c0F">
     <proof
-     prover="7"
+     prover="6"
      timelimit="2"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.00"/>
+     <result status="timeout" time="2.11"/>
     </proof>
     <proof
      prover="1"
@@ -1653,41 +1649,41 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.25"/>
+     <result status="valid" time="0.16"/>
     </proof>
     <proof
      prover="2"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.00"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_BitVector_nth_from_int_low_even_2.v"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="unknown" time="0.57"/>
+     <result status="unknown" time="0.53"/>
     </proof>
    </goal>
    <goal
     name="nth_from_int_low_odd"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="433" loccnumb="8" loccnume="28"
     sum="e97101d47583d206657dff4e17ed51d3"
     proved="true"
     expanded="false"
     shape="ainfix =anthafrom_intV0c0aTrueIainfix =amodV0c2c0NF">
     <proof
-     prover="7"
+     prover="6"
      timelimit="2"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.00"/>
+     <result status="timeout" time="2.11"/>
     </proof>
     <proof
      prover="1"
@@ -1695,20 +1691,20 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.21"/>
+     <result status="valid" time="0.13"/>
     </proof>
     <proof
      prover="2"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.00"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="pow2i"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="436" loccnumb="8" loccnume="13"
     sum="b9297c080d23d5380511c1cf65562670"
     proved="true"
@@ -1718,23 +1714,23 @@
      prover="1"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="timeout" time="10.11"/>
+     <result status="timeout" time="10.08"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_BitVector_pow2i_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.14"/>
+     <result status="valid" time="0.58"/>
     </proof>
    </goal>
    <goal
     name="nth_from_int_0"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="439" loccnumb="8" loccnume="22"
     sum="49ce59a5a80388677eacd82c4ded32c7"
     proved="true"
@@ -1746,48 +1742,48 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="nth_from_int2c_low_even"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="475" loccnumb="8" loccnume="31"
     sum="0f36c1597b117d1e19d696a1483e9fd7"
     proved="true"
     expanded="false"
     shape="ainfix =anthafrom_int2cV0c0aFalseIainfix =amodV0c2c0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_BitVector_nth_from_int2c_low_even_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.11"/>
+     <result status="valid" time="0.56"/>
     </proof>
    </goal>
    <goal
     name="nth_from_int2c_low_odd"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="478" loccnumb="8" loccnume="30"
     sum="4059ef9ffa32a76df358acc145811cc0"
     proved="true"
     expanded="false"
     shape="ainfix =anthafrom_int2cV0c0aTrueIainfix =amodV0c2c0NF">
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_BitVector_nth_from_int2c_low_odd_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.02"/>
+     <result status="valid" time="0.54"/>
     </proof>
    </goal>
    <goal
     name="nth_from_int2c_0"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="481" loccnumb="8" loccnume="24"
     sum="70d9835815960596a1501796d9a8588a"
     proved="true"
@@ -1799,56 +1795,96 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="nth_from_int2c_plus_pow2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="485" loccnumb="8" loccnume="32"
     sum="ad7d6b5fe1513e3c9dd2340ec63e7363"
     proved="false"
     expanded="false"
     shape="ainfix =anthafrom_int2cainfix +V0apow2V2V1anthafrom_int2cV0V1Iainfix &lt;V1V2Aainfix &lt;=c0V1F">
+    <proof
+     prover="6"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="timeout" time="5.11"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="timeout" time="5.03"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="timeout" time="5.02"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="timeout" time="5.03"/>
+    </proof>
+    <proof
+     prover="7"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="timeout" time="5.03"/>
+    </proof>
    </goal>
   </theory>
   <theory
    name="BV32"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="492" loccnumb="7" loccnume="11"
    verified="true"
    expanded="false">
   </theory>
   <theory
    name="BV64"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="501" loccnumb="7" loccnume="11"
    verified="true"
    expanded="false">
   </theory>
   <theory
    name="BV32_64"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="522" loccnumb="7" loccnume="14"
    verified="true"
    expanded="false">
   </theory>
   <theory
    name="BV_double"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="539" loccnumb="7" loccnume="16"
    verified="true"
    expanded="false">
   </theory>
   <theory
    name="TestDouble"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="601" loccnumb="7" loccnume="17"
    verified="true"
    expanded="false">
    <goal
     name="nth_one1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="609" loccnumb="8" loccnume="16"
     sum="4f4ca22125bedb3b9b60c1cecb007f01"
     proved="true"
@@ -1860,12 +1896,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.07"/>
     </proof>
    </goal>
    <goal
     name="nth_one2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="610" loccnumb="8" loccnume="16"
     sum="fba6e00a33cfa0e7d11800bb22e5a5fa"
     proved="true"
@@ -1877,12 +1913,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="nth_one3"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="611" loccnumb="8" loccnume="16"
     sum="010bf8e5c3a68bd34b44bfa0066561cf"
     proved="true"
@@ -1894,12 +1930,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.09"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="sign_one"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="613" loccnumb="8" loccnume="16"
     sum="7582226cb4b0bd7b965fc9cadb2a47e2"
     proved="true"
@@ -1909,9 +1945,9 @@
      prover="2"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.00"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="1"
@@ -1919,12 +1955,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="exp_one"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="614" loccnumb="8" loccnume="15"
     sum="0ec82d16fe4e827be61aa5ec2f1d4a5c"
     proved="true"
@@ -1936,21 +1972,21 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="7.72"/>
+     <result status="valid" time="5.02"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_TestDouble_exp_one_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.03"/>
+     <result status="valid" time="0.60"/>
     </proof>
    </goal>
    <goal
     name="mantissa_one"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="615" loccnumb="8" loccnume="20"
     sum="bad1113e6b18e43a9a8129cb5b451960"
     proved="true"
@@ -1962,12 +1998,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.38"/>
+     <result status="valid" time="0.26"/>
     </proof>
    </goal>
    <goal
     name="double_value_of_1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="617" loccnumb="8" loccnume="25"
     sum="2ac37f4a6b0599d66bc867b1638e11c6"
     proved="true"
@@ -1977,9 +2013,9 @@
      prover="2"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.00"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="1"
@@ -1993,13 +2029,13 @@
   </theory>
   <theory
    name="TestNegAsXOR"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="622" loccnumb="7" loccnume="19"
    verified="true"
    expanded="false">
    <goal
     name="Nth_j"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="632" loccnumb="8" loccnume="13"
     sum="07a1b34440c91dbe42eeb0f2969c5dd9"
     proved="true"
@@ -2019,12 +2055,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.11"/>
+     <result status="valid" time="0.07"/>
     </proof>
    </goal>
    <goal
     name="sign_of_j"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="634" loccnumb="8" loccnume="17"
     sum="f7c354ede730e9414a60a685ba041ce4"
     proved="true"
@@ -2049,7 +2085,7 @@
    </goal>
    <goal
     name="mantissa_of_j"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="635" loccnumb="8" loccnume="21"
     sum="5a4b1310ae3b9d15875fe8df65c956f0"
     proved="true"
@@ -2069,12 +2105,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.22"/>
+     <result status="valid" time="0.15"/>
     </proof>
    </goal>
    <goal
     name="exp_of_j"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="636" loccnumb="8" loccnume="16"
     sum="aa37e69cdbab3f2131611066a8a66687"
     proved="true"
@@ -2094,12 +2130,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.22"/>
+     <result status="valid" time="0.14"/>
     </proof>
    </goal>
    <goal
     name="int_of_bv"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="637" loccnumb="8" loccnume="17"
     sum="1d04361970c56003dae994f4c0bb2d63"
     proved="true"
@@ -2119,12 +2155,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="MainResultBits"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="639" loccnumb="8" loccnume="22"
     sum="dceed52939f21d5dac97ab7063699786"
     proved="true"
@@ -2144,12 +2180,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.11"/>
+     <result status="valid" time="0.07"/>
     </proof>
    </goal>
    <goal
     name="MainResultSign"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="642" loccnumb="8" loccnume="22"
     sum="1b99a48face410652650ba05630c80d2"
     proved="true"
@@ -2161,12 +2197,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="Sign_of_xor_j"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="644" loccnumb="8" loccnume="21"
     sum="30826c11d930d6e90f83ad3952dd3f83"
     proved="true"
@@ -2178,12 +2214,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="Exp_of_xor_j"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="646" loccnumb="8" loccnume="20"
     sum="be1420311e1f57b65c5d95e1a65ee402"
     proved="true"
@@ -2195,12 +2231,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.40"/>
+     <result status="valid" time="0.91"/>
     </proof>
    </goal>
    <goal
     name="Mantissa_of_xor_j"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="648" loccnumb="8" loccnume="25"
     sum="796a6304e6cae0b21f422349e01d0ecb"
     proved="true"
@@ -2220,12 +2256,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.87"/>
+     <result status="valid" time="0.57"/>
     </proof>
    </goal>
    <goal
     name="MainResultZero"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="650" loccnumb="8" loccnume="22"
     sum="1e98ed00dfbc21660b9da9849befef17"
     proved="true"
@@ -2237,12 +2273,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.74"/>
+     <result status="valid" time="1.76"/>
     </proof>
    </goal>
    <goal
     name="sign_neg"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="653" loccnumb="8" loccnume="16"
     sum="f2d4a4e281cb975a67af37d763042dc0"
     proved="true"
@@ -2254,37 +2290,37 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="4.28"/>
+     <result status="valid" time="2.82"/>
     </proof>
    </goal>
    <goal
     name="MainResult"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="655" loccnumb="8" loccnume="18"
     sum="07c09ea843d70dc81974afc4c6df0d66"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix &lt;aexpV0c2047Aainfix &lt;c0aexpV0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="15"
      memlimit="0"
      edited="bitvector1_TestNegAsXOR_MainResult_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.04"/>
+     <result status="valid" time="0.61"/>
     </proof>
    </goal>
   </theory>
   <theory
    name="TestDoubleOfInt"
-   locfile="../why3/tests/bitvector1/../bitvector1.why"
+   locfile="tests/bitvector1/../bitvector1.why"
    loclnum="661" loccnumb="7" loccnume="22"
    verified="false"
    expanded="true">
    <goal
     name="jp0_30"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="682" loccnumb="8" loccnume="14"
     sum="256f16fa09df943ab6313c39374614b7"
     proved="true"
@@ -2296,12 +2332,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.09"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="nth_const1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="698" loccnumb="8" loccnume="18"
     sum="d4004c4cd6c71af10b3e596b25f3854a"
     proved="true"
@@ -2318,7 +2354,7 @@
    </goal>
    <goal
     name="nth_const2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="699" loccnumb="8" loccnume="18"
     sum="5dee62d23ccb40ec5d40c1597bbd1d89"
     proved="true"
@@ -2330,12 +2366,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.04"/>
     </proof>
    </goal>
    <goal
     name="nth_const3"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="700" loccnumb="8" loccnume="18"
     sum="e30e835732c9284f02510ce599443ca6"
     proved="true"
@@ -2347,12 +2383,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.55"/>
+     <result status="valid" time="1.02"/>
     </proof>
    </goal>
    <goal
     name="nth_const4"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="701" loccnumb="8" loccnume="18"
     sum="33a46ed3a16663d8fd5bc3aa3165a233"
     proved="true"
@@ -2364,12 +2400,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.60"/>
+     <result status="valid" time="1.07"/>
     </proof>
    </goal>
    <goal
     name="nth_const5"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="702" loccnumb="8" loccnume="18"
     sum="386efa0cbb8b1496c6838803b89816b4"
     proved="true"
@@ -2381,12 +2417,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.63"/>
+     <result status="valid" time="1.09"/>
     </proof>
    </goal>
    <goal
     name="nth_const6"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="703" loccnumb="8" loccnume="18"
     sum="81cd040edd829b2357b2e9d6c1317797"
     proved="true"
@@ -2398,12 +2434,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.62"/>
+     <result status="valid" time="1.06"/>
     </proof>
    </goal>
    <goal
     name="nth_const7"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="704" loccnumb="8" loccnume="18"
     sum="ddf37306bee048cc9ae0eee70cbb5381"
     proved="true"
@@ -2415,12 +2451,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.59"/>
+     <result status="valid" time="1.09"/>
     </proof>
    </goal>
    <goal
     name="nth_const8"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="705" loccnumb="8" loccnume="18"
     sum="0b964b78d9c1c2b7469e2b7e23aaefaa"
     proved="true"
@@ -2437,7 +2473,7 @@
    </goal>
    <goal
     name="nth_const9"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="706" loccnumb="8" loccnume="18"
     sum="cb3e81fa600947eba00c29c3654d6c79"
     proved="true"
@@ -2449,12 +2485,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.06"/>
+     <result status="valid" time="0.04"/>
     </proof>
    </goal>
    <goal
     name="sign_const"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="708" loccnumb="8" loccnume="18"
     sum="5f3770394802a8bdd75c4d45c330fdec"
     proved="true"
@@ -2466,16 +2502,16 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="exp_const"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="710" loccnumb="8" loccnume="17"
     sum="2a0f413ac1c3812a77bdc079631adcbb"
     proved="true"
-    expanded="true"
+    expanded="false"
     shape="ainfix =aexpaconstc1075">
     <proof
      prover="1"
@@ -2483,21 +2519,21 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="10.09"/>
+     <result status="timeout" time="10.08"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_exp_const_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.61"/>
+     <result status="valid" time="0.95"/>
     </proof>
    </goal>
    <goal
     name="to_nat_mantissa_1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="712" loccnumb="8" loccnume="25"
     sum="dce268d7e789e4ba8780f5fc5db73629"
     proved="true"
@@ -2509,12 +2545,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.05"/>
     </proof>
    </goal>
    <goal
     name="mantissa_const_nth2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="714" loccnumb="8" loccnume="27"
     sum="02cab213bdd1cf475d3dd42bce679cc0"
     proved="true"
@@ -2531,7 +2567,7 @@
    </goal>
    <goal
     name="mantissa_const_to_nat51"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="717" loccnumb="8" loccnume="31"
     sum="df576de9da612b4b66a57a77e0d60ec9"
     proved="true"
@@ -2543,12 +2579,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.20"/>
+     <result status="valid" time="0.15"/>
     </proof>
    </goal>
    <goal
     name="mantissa_const"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="720" loccnumb="8" loccnume="22"
     sum="865cafb40a99949daf8c8539420a899a"
     proved="true"
@@ -2560,7 +2596,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.04"/>
     </proof>
     <proof
      prover="1"
@@ -2568,12 +2604,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.89"/>
+     <result status="valid" time="0.57"/>
     </proof>
    </goal>
    <goal
     name="real1075m1023"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="722" loccnumb="8" loccnume="21"
     sum="71383555f7eceb15b27cab1e547057be"
     proved="true"
@@ -2583,12 +2619,12 @@
      prover="1"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="timeout" time="10.01"/>
+     <result status="timeout" time="10.07"/>
     </proof>
     <proof
-     prover="6"
+     prover="5"
      timelimit="20"
      memlimit="0"
      obsolete="false"
@@ -2598,7 +2634,7 @@
    </goal>
    <goal
     name="real1075m1023_2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="724" loccnumb="8" loccnume="23"
     sum="3440ba6b7c47313549769c9475a27582"
     proved="true"
@@ -2610,12 +2646,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.02"/>
     </proof>
    </goal>
    <goal
     name="real52_a_m52"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="726" loccnumb="8" loccnume="20"
     sum="32a774be03a493aed1920f1acbcfe2f1"
     proved="true"
@@ -2623,28 +2659,28 @@
     shape="ainfix =ainfix *.ainfix *.apow2ainfix -c1075c1023apow2c31apow2aprefix -c52apow2c31">
     <proof
      prover="1"
-     timelimit="30"
+     timelimit="40"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="19.52"/>
+     <result status="valid" time="12.51"/>
     </proof>
    </goal>
    <goal
     name="const_value0"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="728" loccnumb="8" loccnume="20"
     sum="1a9c06809da7492cd2442bdd3957ed81"
     proved="true"
     expanded="false"
     shape="ainfix =aconst_as_doubleainfix *.ainfix *.c1.0apow2ainfix -c1075c1023ainfix +.c1.0ainfix *.apow2c31apow2aprefix -c52">
     <proof
-     prover="7"
+     prover="6"
      timelimit="20"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="timeout" time="20.18"/>
+     <result status="timeout" time="20.10"/>
     </proof>
     <proof
      prover="1"
@@ -2652,40 +2688,40 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.35"/>
+     <result status="valid" time="0.24"/>
     </proof>
     <proof
      prover="2"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.04"/>
+     <result status="valid" time="0.08"/>
     </proof>
    </goal>
    <goal
     name="const_value"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="731" loccnumb="8" loccnume="19"
     sum="a8ad4dd5ecd3ae37af4643bb651a4343"
     proved="true"
     expanded="false"
     shape="ainfix =aconst_as_doubleainfix +.apow2c52apow2c31">
     <proof
-     prover="7"
+     prover="6"
      timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.20"/>
+     <result status="valid" time="0.12"/>
     </proof>
     <proof
      prover="2"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="failure" time="0.04"/>
+     <result status="valid" time="0.04"/>
     </proof>
     <proof
      prover="1"
@@ -2699,14 +2735,14 @@
      prover="4"
      timelimit="20"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false"><unedited/>
      
     </proof>
    </goal>
    <goal
     name="nth_0_30"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="757" loccnumb="8" loccnume="16"
     sum="6c69e748ddc090f99c61d03e3c611386"
     proved="true"
@@ -2726,12 +2762,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.68"/>
+     <result status="valid" time="0.46"/>
     </proof>
    </goal>
    <goal
     name="nth_jpxor_0_30"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="759" loccnumb="8" loccnume="22"
     sum="83e888fa6135392d87fca54df26f47d0"
     proved="true"
@@ -2751,12 +2787,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.11"/>
+     <result status="valid" time="0.09"/>
     </proof>
    </goal>
    <goal
     name="nth_var31"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="761" loccnumb="8" loccnume="17"
     sum="385e09a03f600bdce9c13a65cbe4f55a"
     proved="true"
@@ -2776,12 +2812,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.64"/>
+     <result status="valid" time="1.10"/>
     </proof>
    </goal>
    <goal
     name="to_nat_sub_0_30"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="764" loccnumb="8" loccnume="23"
     sum="be8bc732bd62c8d9f36612565509df3f"
     proved="true"
@@ -2801,12 +2837,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.34"/>
+     <result status="valid" time="0.22"/>
     </proof>
    </goal>
    <goal
     name="jpxorx_pos"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="771" loccnumb="8" loccnume="18"
     sum="86ca976d13fa6b76041ce52c57b8170b"
     proved="true"
@@ -2818,42 +2854,42 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.30"/>
+     <result status="valid" time="0.21"/>
     </proof>
    </goal>
    <goal
     name="from_int2c_to_nat_sub_gen"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="778" loccnumb="8" loccnume="33"
     sum="62161f6f5b9c90eafc7f037846c856c5"
     proved="false"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ato_nat_subafrom_int2cV1ainfix -V0c1c0V1Iainfix &lt;V1apow2V0Aainfix &lt;=c0V1FIainfix &lt;=V0c30Aainfix &lt;=c0V0F">
     <proof
-     prover="5"
-     timelimit="10"
-     memlimit="0"
+     prover="4"
+     timelimit="5"
+     memlimit="1000"
      edited="bitvector1_TestDoubleOfInt_from_int2c_to_nat_sub_gen_1.v"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="1.11"/>
+     <result status="unknown" time="0.89"/>
     </proof>
    </goal>
    <goal
     name="from_int2c_to_nat_sub"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="783" loccnumb="8" loccnume="29"
     sum="cb5841b82e8cb4c8a9e08ab053d7860c"
     proved="false"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ato_nat_subafrom_int2cV0c30c0V0Iainfix &gt;=V0c0Aais_int32V0F">
     <proof
-     prover="7"
-     timelimit="10"
-     memlimit="0"
+     prover="6"
+     timelimit="5"
+     memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="10.72"/>
+     <result status="timeout" time="5.04"/>
     </proof>
     <proof
      prover="0"
@@ -2865,44 +2901,44 @@
     </proof>
     <proof
      prover="2"
-     timelimit="10"
-     memlimit="0"
+     timelimit="5"
+     memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="failure" time="0.32"/>
+     <result status="highfailure" time="0.18"/>
     </proof>
     <proof
      prover="1"
-     timelimit="10"
-     memlimit="0"
+     timelimit="5"
+     memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="10.21"/>
+     <result status="timeout" time="5.04"/>
     </proof>
     <proof
      prover="3"
-     timelimit="10"
-     memlimit="0"
+     timelimit="5"
+     memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="failure" time="0.72"/>
+     <result status="highfailure" time="0.42"/>
     </proof>
     <proof
-     prover="8"
-     timelimit="10"
-     memlimit="0"
+     prover="7"
+     timelimit="5"
+     memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="10.04"/>
+     <result status="timeout" time="5.04"/>
     </proof>
    </goal>
    <goal
     name="lemma1_pos"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="786" loccnumb="8" loccnume="18"
     sum="855b8663aa4abce854b96f525fe1c89b"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ato_nat_subajpxorV0c31c0ainfix +apow2c31V0Iainfix &gt;=V0c0Aais_int32V0F">
     <proof
      prover="1"
@@ -2910,74 +2946,106 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="7.88"/>
+     <result status="valid" time="5.35"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_lemma1_pos_1.v"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="1.22"/>
+     <result status="unknown" time="0.66"/>
     </proof>
    </goal>
    <goal
     name="to_nat_sub_0_30_neg"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="790" loccnumb="8" loccnume="27"
     sum="df3d1ed25863af4db80bbd6cbf9271a3"
     proved="true"
     expanded="false"
     shape="ainfix =ato_nat_subabw_xoraj&apos;afrom_int2cV0c30c0ato_nat_subafrom_int2cV0c30c0Iainfix &lt;V0c0Aais_int32V0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_to_nat_sub_0_30_neg_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.21"/>
+     <result status="valid" time="0.64"/>
     </proof>
    </goal>
    <goal
     name="to_nat_sub_0_30_neg1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="793" loccnumb="8" loccnume="28"
     sum="4a4148ba6a3d73832dfe606fa8ef8464"
     proved="false"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ato_nat_subafrom_int2cV0c30c0ainfix +apow2c31V0Iainfix &lt;V0c0Aais_int32V0F">
+    <proof
+     prover="6"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="timeout" time="5.03"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="highfailure" time="0.15"/>
+    </proof>
     <proof
      prover="1"
-     timelimit="14"
-     memlimit="0"
-     obsolete="true"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
      archived="false">
-     <result status="timeout" time="14.02"/>
+     <result status="timeout" time="5.04"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="highfailure" time="0.35"/>
+    </proof>
+    <proof
+     prover="7"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="timeout" time="5.03"/>
     </proof>
    </goal>
    <goal
     name="lemma1_neg"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="796" loccnumb="8" loccnume="18"
     sum="1731b8b313b5ba14c08ddf2565fd72cc"
     proved="false"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ato_nat_subajpxorV0c31c0ainfix +apow2c31V0Iainfix &lt;V0c0Aais_int32V0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      edited="bitvector1_TestDoubleOfInt_lemma1_neg_1.v"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="1.11"/>
+     <result status="unknown" time="0.64"/>
     </proof>
    </goal>
    <goal
     name="lemma1"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="800" loccnumb="8" loccnume="14"
     sum="0c6093611ddd2efcd97e810e54746d86"
     proved="true"
@@ -2989,12 +3057,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.04"/>
     </proof>
    </goal>
    <goal
     name="nth_var_0_31"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="807" loccnumb="8" loccnume="20"
     sum="88e5217a2bbc59feaa5558a7bfe99f15"
     proved="true"
@@ -3006,30 +3074,30 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.26"/>
+     <result status="valid" time="1.58"/>
     </proof>
    </goal>
    <goal
     name="to_nat_bv32_bv64_aux"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="809" loccnumb="8" loccnume="28"
     sum="aa7b3a04f3e8f54b0cdcacb9b80555e4"
     proved="true"
     expanded="false"
     shape="ainfix =ato_nat_subaconcatV0V1V2c0ato_nat_subV1V2c0Iainfix &lt;V2c32Aainfix &lt;=c0V2FFF">
     <proof
-     prover="5"
+     prover="4"
      timelimit="10"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_to_nat_bv32_bv64_aux_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.64"/>
+     <result status="valid" time="0.85"/>
     </proof>
    </goal>
    <goal
     name="to_nat_bv32_bv64"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="810" loccnumb="8" loccnume="24"
     sum="022b51f6ee685e3a244545ed8ab676ae"
     proved="true"
@@ -3041,30 +3109,30 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.04"/>
     </proof>
    </goal>
    <goal
     name="to_nat_var_0_31"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="812" loccnumb="8" loccnume="23"
     sum="448286e6565a904f085af11a72cb052a"
     proved="true"
     expanded="false"
     shape="ainfix =ato_nat_subavarV0c31c0ato_nat_subajpxorV0c31c0Iais_int32V0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_to_nat_var_0_31_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.30"/>
+     <result status="valid" time="0.66"/>
     </proof>
    </goal>
    <goal
     name="nth_var32to63"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="814" loccnumb="8" loccnume="21"
     sum="bce5e882598871677b3ca8f5deae89cc"
     proved="true"
@@ -3084,12 +3152,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.05"/>
+     <result status="valid" time="1.38"/>
     </proof>
    </goal>
    <goal
     name="nth_var3"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="817" loccnumb="8" loccnume="16"
     sum="8718d3c5b47baed2ceee57514497e5a8"
     proved="true"
@@ -3105,34 +3173,34 @@
     </proof>
     <proof
      prover="1"
-     timelimit="20"
+     timelimit="28"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="13.53"/>
+     <result status="valid" time="8.90"/>
     </proof>
    </goal>
    <goal
     name="lemma2"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="819" loccnumb="8" loccnume="14"
     sum="0e680141ab92a3d9934f0e1ef4329c86"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaavarV0ainfix +apow2c31V0Iais_int32V0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="30"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_lemma2_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.27"/>
+     <result status="valid" time="0.66"/>
     </proof>
    </goal>
    <goal
     name="nth_var4"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="825" loccnumb="8" loccnume="16"
     sum="80379f624c8b0f92d495d5bd2209b176"
     proved="true"
@@ -3140,16 +3208,16 @@
     shape="ainfix =anthavarV0V1aTrueIainfix &lt;=V1c53Aainfix &lt;=c52V1FF">
     <proof
      prover="1"
-     timelimit="23"
+     timelimit="32"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="15.86"/>
+     <result status="valid" time="10.50"/>
     </proof>
    </goal>
    <goal
     name="nth_var5"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="826" loccnumb="8" loccnume="16"
     sum="45ad1d1f57c828a50a30ee0b875d151f"
     proved="true"
@@ -3161,12 +3229,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="12.83"/>
+     <result status="valid" time="8.84"/>
     </proof>
    </goal>
    <goal
     name="nth_var6"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="827" loccnumb="8" loccnume="16"
     sum="dccb54542fd53a9656e3dd93266f8f89"
     proved="true"
@@ -3178,12 +3246,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="14.96"/>
+     <result status="valid" time="10.46"/>
     </proof>
    </goal>
    <goal
     name="nth_var7"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="828" loccnumb="8" loccnume="16"
     sum="a0e9f273647bdc778b97baadbbba6245"
     proved="true"
@@ -3195,24 +3263,24 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="12.65"/>
+     <result status="valid" time="8.84"/>
     </proof>
    </goal>
    <goal
     name="nth_var8"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="829" loccnumb="8" loccnume="16"
     sum="80417e5ade242e3a4eac10f6f5fb6aa0"
     proved="true"
     expanded="false"
     shape="ainfix =anthavarV0c62aTrueF">
     <proof
-     prover="7"
+     prover="6"
      timelimit="5"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.22"/>
+     <result status="valid" time="0.13"/>
     </proof>
     <proof
      prover="1"
@@ -3220,30 +3288,30 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.21"/>
+     <result status="valid" time="0.13"/>
     </proof>
    </goal>
    <goal
     name="lemma3"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="831" loccnumb="8" loccnume="14"
     sum="573c52d92f482921f80d8f7da844f8ce"
     proved="true"
     expanded="false"
     shape="ainfix =aexpavarV0c1075F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_lemma3_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.62"/>
+     <result status="valid" time="0.93"/>
     </proof>
    </goal>
    <goal
     name="nth_var9"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="837" loccnumb="8" loccnume="16"
     sum="e831093547176c93f6bebd2b1a5f6e2c"
     proved="true"
@@ -3255,12 +3323,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.48"/>
+     <result status="valid" time="0.34"/>
     </proof>
    </goal>
    <goal
     name="lemma4"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="839" loccnumb="7" loccnume="13"
     sum="2e42eaf4cae66a429aca1ade9fd57682"
     proved="true"
@@ -3280,10 +3348,10 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.07"/>
+     <result status="valid" time="0.06"/>
     </proof>
     <proof
-     prover="8"
+     prover="7"
      timelimit="5"
      memlimit="0"
      obsolete="false"
@@ -3293,7 +3361,7 @@
    </goal>
    <goal
     name="sign_var"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="844" loccnumb="8" loccnume="16"
     sum="75c6743ffcc57d530e501b34f49e688f"
     proved="true"
@@ -3310,25 +3378,25 @@
    </goal>
    <goal
     name="var_value0"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="846" loccnumb="8" loccnume="18"
     sum="05a4291e8318d8c1bf942ef5ffead31f"
     proved="true"
     expanded="false"
     shape="ainfix =avar_as_doubleV0ainfix *.apow2ainfix -c1075c1023ainfix +.c1.0ainfix *.afrom_intainfix +apow2c31V0apow2aprefix -c52Iais_int32V0F">
     <proof
-     prover="5"
+     prover="4"
      timelimit="20"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_var_value0_3.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.20"/>
+     <result status="valid" time="0.67"/>
     </proof>
    </goal>
    <goal
     name="from_int_sum"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="850" loccnumb="8" loccnume="20"
     sum="ba03097a58b973e69a51d7845de21285"
     proved="true"
@@ -3340,12 +3408,12 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.09"/>
+     <result status="valid" time="0.06"/>
     </proof>
    </goal>
    <goal
     name="var_value3"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="853" loccnumb="8" loccnume="18"
     sum="52ff305f9de7bc0f32e2cf3eb20368de"
     proved="true"
@@ -3355,23 +3423,23 @@
      prover="1"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="timeout" time="10.01"/>
+     <result status="timeout" time="10.08"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="20"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_var_value3_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.17"/>
+     <result status="valid" time="0.67"/>
     </proof>
    </goal>
    <goal
     name="distr_pow52"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="857" loccnumb="8" loccnume="19"
     sum="e37ab51b48678dfe7ea12f1287410e5b"
     proved="true"
@@ -3381,23 +3449,23 @@
      prover="1"
      timelimit="10"
      memlimit="0"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <result status="timeout" time="10.02"/>
+     <result status="timeout" time="10.07"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="15"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_distr_pow52_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.21"/>
+     <result status="valid" time="0.66"/>
     </proof>
    </goal>
    <goal
     name="var_value4"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="860" loccnumb="8" loccnume="18"
     sum="bc1f2f38dbc500c26e96809a364e0266"
     proved="true"
@@ -3405,25 +3473,25 @@
     shape="ainfix =avar_as_doubleV0ainfix +.ainfix +.apow2c52afrom_intapow2c31afrom_intV0Iais_int32V0F">
     <proof
      prover="1"
-     timelimit="33"
+     timelimit="40"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="19.61"/>
+     <result status="valid" time="13.38"/>
     </proof>
     <proof
-     prover="5"
+     prover="4"
      timelimit="5"
      memlimit="0"
      edited="bitvector1_TestDoubleOfInt_var_value4_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.15"/>
+     <result status="valid" time="0.67"/>
     </proof>
    </goal>
    <goal
     name="pow31"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="863" loccnumb="8" loccnume="13"
     sum="6ef74f1d506a7d144fbe3de9f2f31f4f"
     proved="true"
@@ -3443,20 +3511,20 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.06"/>
+     <result status="valid" time="0.05"/>
     </proof>
     <proof
-     prover="8"
+     prover="7"
      timelimit="5"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="5.11"/>
+     <result status="timeout" time="5.03"/>
     </proof>
    </goal>
    <goal
     name="lemma5"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="865" loccnumb="8" loccnume="14"
     sum="fb7ca47f636dd4bd7f8f24cb8a08df27"
     proved="true"
@@ -3468,24 +3536,24 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.04"/>
     </proof>
    </goal>
    <goal
     name="MainResult"
-    locfile="../why3/tests/bitvector1/../bitvector1.why"
+    locfile="tests/bitvector1/../bitvector1.why"
     loclnum="875" loccnumb="8" loccnume="18"
     sum="e488945ab885a1890046d7f229e9ffee"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_int32V0afrom_intV0Iais_int32V0F">
     <proof
-     prover="7"
+     prover="6"
      timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.18"/>
+     <result status="valid" time="0.75"/>
     </proof>
     <proof
      prover="0"
@@ -3501,7 +3569,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.30"/>
+     <result status="valid" time="0.22"/>
     </proof>
    </goal>
   </theory>