diff options
| -rw-r--r-- | kvx/FPDivision64.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 6894460f..9ed12064 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1108,7 +1108,7 @@ Qed. Definition step2_real_div_long a b := Val.mulf (Val.maketotal (Val.floatoflong a)) (approx_inv_longu b). -Definition smalla_thresh := 35184372088832%Z. +Definition smalla_thresh := 34184372088832%Z. Lemma step2_real_div_long_smalla_correct : forall (a b : int64) @@ -1116,7 +1116,7 @@ Lemma step2_real_div_long_smalla_correct : (b_NOT0 : (0 < Int64.unsigned b)%Z), exists (q : float), (step2_real_div_long (Vlong a) (Vlong b)) = Vfloat q /\ - (Rabs ((B2R _ _ q) - (IZR (Int64.signed a)) / (IZR (Int64.unsigned b))) <= (255/256))%R. + (Rabs ((B2R _ _ q) - (IZR (Int64.signed a)) / (IZR (Int64.unsigned b))) <= (32767/65536))%R. Proof. intros. unfold step2_real_div_long. |