Turn 64-bit integer division and modulus by constants into multiply-high

This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
author: Xavier Leroy <xavier.leroy@inria.fr> 2016-10-04 15:52:16 +0200
committer: Xavier Leroy <xavier.leroy@inria.fr> 2016-10-04 15:52:16 +0200
commit: d2af79a77ed2936ff0ed90cadf8e48637d774d4c (patch)
tree: 09300943e12a98ae80598c79d455b31725271ead
parent: a44893028eb1dd434c68001234ad56d030205a8e (diff)
download: compcert-kvx-d2af79a77ed2936ff0ed90cadf8e48637d774d4c.tar.gz
compcert-kvx-d2af79a77ed2936ff0ed90cadf8e48637d774d4c.zip
29 files changed, 3031 insertions, 25 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 1fc0b689..5cc66322 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -206,14 +206,23 @@ Context {hf: helper_functions}.
 Definition modl_from_divl (equo: expr) (n: int64) :=
   subl (Eletvar O) (mullimm n equo).
 
+Definition divlu_mull (p: Z) (m: Z) :=
+  shrluimm (mullhu (Eletvar O) (Int64.repr m)) (Int.repr p).
+
 Definition divlu (e1 e2: expr) :=
   match is_longconst e2, is_longconst e1 with
   | Some n2, Some n1 => longconst (Int64.divu n1 n2)
   | Some n2, _ =>
       match Int64.is_power2' n2 with
       | Some l => shrluimm e1 l
-      | None   => divlu_base e1 e2
-      end (* TODO: multiply-high *)
+      | None   => if optim_for_size tt then
+                    divlu_base e1 e2
+                  else
+                    match divlu_mul_params (Int64.unsigned n2) with
+                    | None => divlu_base e1 e2
+                    | Some(p, m) => Elet e1 (divlu_mull p m)
+                    end
+      end
   | _, _ => divlu_base e1 e2
   end.
 
@@ -223,19 +232,41 @@ Definition modlu (e1 e2: expr) :=
   | Some n2, _ =>
       match Int64.is_power2 n2 with
       | Some l => andl e1 (longconst (Int64.sub n2 Int64.one))
-      | None   => modlu_base e1 e2
+      | None   => if optim_for_size tt then
+                    modlu_base e1 e2
+                  else
+                    match divlu_mul_params (Int64.unsigned n2) with
+                    | None => modlu_base e1 e2
+                    | Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2)
+                    end
       end
   | _, _ => modlu_base e1 e2
   end.
 
+Definition divls_mull (p: Z) (m: Z) :=
+  let e2 := 
+    mullhs (Eletvar O) (Int64.repr m) in
+  let e3 :=
+    if zlt m Int64.half_modulus then e2 else addl e2 (Eletvar O) in
+  addl (shrlimm e3 (Int.repr p))
+       (shrluimm (Eletvar O) (Int.repr (Int64.zwordsize - 1))).
+
 Definition divls (e1 e2: expr) :=
   match is_longconst e2, is_longconst e1 with
   | Some n2, Some n1 => longconst (Int64.divs n1 n2)
   | Some n2, _ =>
       match Int64.is_power2' n2 with
-      | Some l => if Int.ltu l (Int.repr 63) then shrxlimm e1 l else divls_base e1 e2
-      | None   => divls_base e1 e2
-      end (* TODO: multiply-high *)
+      | Some l => if Int.ltu l (Int.repr 63)
+                  then shrxlimm e1 l
+                  else divls_base e1 e2
+      | None   => if optim_for_size tt then
+                    divls_base e1 e2
+                  else
+                    match divls_mul_params (Int64.signed n2) with
+                    | None => divls_base e1 e2
+                    | Some(p, m) => Elet e1 (divls_mull p m)
+                    end
+      end
   | _, _ => divls_base e1 e2
   end.
 
@@ -247,7 +278,13 @@ Definition modls (e1 e2: expr) :=
       | Some l => if Int.ltu l (Int.repr 63)
                   then Elet e1 (modl_from_divl (shrxlimm (Eletvar O) l) n2)
                   else modls_base e1 e2
-      | None   => modls_base e1 e2
+      | None   => if optim_for_size tt then
+                    modls_base e1 e2
+                  else
+                    match divls_mul_params (Int64.signed n2) with
+                    | None => modls_base e1 e2
+                    | Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2)
+                    end
       end
   | _, _ => modls_base e1 e2
   end.
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 441f69b1..41db3c70 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -317,6 +317,165 @@ Proof.
   assert (32 < Int.max_unsigned) by (compute; auto). omega.
 Qed.
 
+(** Same, for 64-bit integers *)
+
+Lemma divls_mul_params_sound:
+  forall d m p,
+  divls_mul_params d = Some(p, m) ->
+  0 <= m < Int64.modulus /\ 0 <= p < 64 /\
+  forall n,
+  Int64.min_signed <= n <= Int64.max_signed ->
+  Z.quot n d = Zdiv (m * n) (two_p (64 + p)) + (if zlt n 0 then 1 else 0).
+Proof with (try discriminate).
+  unfold divls_mul_params; intros d m' p'.
+  destruct (find_div_mul_params Int64.wordsize
+               (Int64.half_modulus - Int64.half_modulus mod d - 1) d 64)
+  as [[p m] | ]...
+  generalize (p - 64). intro p1.  
+  destruct (zlt 0 d)...
+  destruct (zlt (two_p (64 + p1)) (m * d))...
+  destruct (zle (m * d) (two_p (64 + p1) + two_p (p1 + 1)))...
+  destruct (zle 0 m)...
+  destruct (zlt m Int64.modulus)...
+  destruct (zle 0 p1)...
+  destruct (zlt p1 64)...
+  intros EQ; inv EQ. 
+  split. auto. split. auto. intros.
+  replace (64 + p') with (63 + (p' + 1)) by omega.
+  apply Zquot_mul; try omega.
+  replace (63 + (p' + 1)) with (64 + p') by omega. omega.
+  change (Int64.min_signed <= n < Int64.half_modulus).
+  unfold Int64.max_signed in H. omega.
+Qed.
+
+Lemma divlu_mul_params_sound:
+  forall d m p,
+  divlu_mul_params d = Some(p, m) ->
+  0 <= m < Int64.modulus /\ 0 <= p < 64 /\
+  forall n,
+  0 <= n < Int64.modulus ->
+  Zdiv n d = Zdiv (m * n) (two_p (64 + p)).
+Proof with (try discriminate).
+  unfold divlu_mul_params; intros d m' p'.
+  destruct (find_div_mul_params Int64.wordsize
+               (Int64.modulus - Int64.modulus mod d - 1) d 64)
+  as [[p m] | ]...
+  generalize (p - 64); intro p1.
+  destruct (zlt 0 d)...
+  destruct (zle (two_p (64 + p1)) (m * d))...
+  destruct (zle (m * d) (two_p (64 + p1) + two_p p1))...
+  destruct (zle 0 m)...
+  destruct (zlt m Int64.modulus)...
+  destruct (zle 0 p1)...
+  destruct (zlt p1 64)...
+  intros EQ; inv EQ.
+  split. auto. split. auto. intros.
+  apply Zdiv_mul_pos; try omega. assumption.
+Qed.
+
+Remark int64_shr'_div_two_p:
+  forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)).
+Proof.
+  intros; unfold Int64.shr'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+Qed.
+
+Lemma divls_mul_shift_gen:
+  forall x y m p,
+  divls_mul_params (Int64.signed y) = Some(p, m) ->
+  0 <= m < Int64.modulus /\ 0 <= p < 64 /\
+  Int64.divs x y = Int64.add (Int64.shr' (Int64.repr ((Int64.signed x * m) / Int64.modulus)) (Int.repr p))
+                             (Int64.shru x (Int64.repr 63)).
+Proof.
+  intros. set (n := Int64.signed x). set (d := Int64.signed y) in *.
+  exploit divls_mul_params_sound; eauto. intros (A & B & C).
+  split. auto. split. auto.
+  unfold Int64.divs. fold n; fold d. rewrite C by (apply Int64.signed_range).
+  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv.
+  rewrite Int64.shru_lt_zero. unfold Int64.add. apply Int64.eqm_samerepr. apply Int64.eqm_add.
+  rewrite int64_shr'_div_two_p. apply Int64.eqm_unsigned_repr_r. apply Int64.eqm_refl2.
+  rewrite Int.unsigned_repr. f_equal.
+  rewrite Int64.signed_repr. rewrite Int64.modulus_power. f_equal. ring.
+  cut (Int64.min_signed <= n * m / Int64.modulus < Int64.half_modulus).
+  unfold Int64.max_signed; omega.
+  apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos.
+  apply Int64.modulus_pos.
+  split. apply Zle_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega.
+  apply Zmult_le_compat_r. unfold n; generalize (Int64.signed_range x); tauto. tauto.
+  apply Zle_lt_trans with (Int64.half_modulus * m).
+  apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto.
+  apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto.
+  assert (64 < Int.max_unsigned) by (compute; auto). omega.
+  unfold Int64.lt; fold n. rewrite Int64.signed_zero. destruct (zlt n 0); apply Int64.eqm_unsigned_repr.
+  apply two_p_gt_ZERO. omega.
+  apply two_p_gt_ZERO. omega.
+Qed.
+
+Theorem divls_mul_shift_1:
+  forall x y m p,
+  divls_mul_params (Int64.signed y) = Some(p, m) ->
+  m < Int64.half_modulus ->
+  0 <= p < 64 /\
+  Int64.divs x y = Int64.add (Int64.shr' (Int64.mulhs x (Int64.repr m)) (Int.repr p))
+                             (Int64.shru' x (Int.repr 63)).
+Proof.
+  intros. exploit divls_mul_shift_gen; eauto. instantiate (1 := x).
+  intros (A & B & C). split. auto. rewrite C.
+  unfold Int64.mulhs. rewrite Int64.signed_repr. auto.
+  generalize Int64.min_signed_neg; unfold Int64.max_signed; omega.
+Qed.
+
+Theorem divls_mul_shift_2:
+  forall x y m p,
+  divls_mul_params (Int64.signed y) = Some(p, m) ->
+  m >= Int64.half_modulus ->
+  0 <= p < 64 /\
+  Int64.divs x y = Int64.add (Int64.shr' (Int64.add (Int64.mulhs x (Int64.repr m)) x) (Int.repr p))
+                             (Int64.shru' x (Int.repr 63)).
+Proof.
+  intros. exploit divls_mul_shift_gen; eauto. instantiate (1 := x).
+  intros (A & B & C). split. auto. rewrite C. f_equal. f_equal.
+  rewrite Int64.add_signed. unfold Int64.mulhs. set (n := Int64.signed x).
+  transitivity (Int64.repr (n * (m - Int64.modulus) / Int64.modulus + n)).
+  f_equal.
+  replace (n * (m - Int64.modulus)) with (n * m +  (-n) * Int64.modulus) by ring.
+  rewrite Z_div_plus. ring. apply Int64.modulus_pos.
+  apply Int64.eqm_samerepr. apply Int64.eqm_add; auto with ints.
+  apply Int64.eqm_sym. eapply Int64.eqm_trans. apply Int64.eqm_signed_unsigned.
+  apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2. f_equal. f_equal.
+  rewrite Int64.signed_repr_eq. rewrite Zmod_small by assumption.
+  apply zlt_false. omega.
+Qed.
+
+Remark int64_shru'_div_two_p:
+  forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)).
+Proof.
+  intros; unfold Int64.shru'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+Qed.
+
+Theorem divlu_mul_shift:
+  forall x y m p,
+  divlu_mul_params (Int64.unsigned y) = Some(p, m) ->
+  0 <= p < 64 /\
+  Int64.divu x y = Int64.shru' (Int64.mulhu x (Int64.repr m)) (Int.repr p).
+Proof.
+  intros. exploit divlu_mul_params_sound; eauto. intros (A & B & C).
+  split. auto.
+  rewrite int64_shru'_div_two_p. rewrite Int.unsigned_repr.
+  unfold Int64.divu, Int64.mulhu. f_equal. rewrite C by apply Int64.unsigned_range.
+  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega).
+  f_equal. rewrite (Int64.unsigned_repr m).
+  rewrite Int64.unsigned_repr. f_equal. ring.
+  cut (0 <= Int64.unsigned x * m / Int64.modulus < Int64.modulus).
+  unfold Int64.max_unsigned; omega.
+  apply Zdiv_interval_1. omega. compute; auto. compute; auto.
+  split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); omega. omega.
+  apply Zle_lt_trans with (Int64.modulus * m).
+  apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); omega. omega.
+  apply Zmult_lt_compat_l. compute; auto. omega.
+  unfold Int64.max_unsigned; omega.
+  assert (64 < Int.max_unsigned) by (compute; auto). omega.
+Qed.
+
 (** * Correctness of the smart constructors for division and modulus *)
 
 Section CMCONSTRS.
@@ -559,6 +718,22 @@ Proof.
   simpl in B1; inv B1. simpl in B2; inv B2. exact A2.
 Qed.
 
+Lemma eval_divlu_mull:
+  forall le x y p M,
+  divlu_mul_params (Int64.unsigned y) = Some(p, M) ->
+  nth_error le O = Some (Vlong x) ->
+  eval_expr ge sp e m le (divlu_mull p M) (Vlong (Int64.divu x y)).
+Proof.
+  intros. unfold divlu_mull. exploit (divlu_mul_shift x); eauto. intros [A B].
+  assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)) by (constructor; auto).
+  exploit eval_mullhu. eauto. eexact A0. instantiate (1 := Int64.repr M). intros (v1 & A1 & B1).
+  exploit eval_shrluimm. eauto. eexact A1. instantiate (1 := Int.repr p). intros (v2 & A2 & B2).
+  simpl in B1; inv B1. simpl in B2. replace (Int.ltu (Int.repr p) Int64.iwordsize') with true in B2. inv B2.
+  rewrite B. assumption.
+  unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto.
+  assert (64 < Int.max_unsigned) by (compute; auto). omega.
+Qed.
+
 Theorem eval_divlu:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
@@ -575,7 +750,12 @@ Proof.
   econstructor; split. apply eval_longconst. constructor.
 + destruct (Int64.is_power2' n2) as [l|] eqn:POW.
 * exploit Val.divlu_pow2; eauto. intros EQ; subst z. apply eval_shrluimm; auto.
-* eapply eval_divlu_base; eauto.     
+* destruct (Compopts.optim_for_size tt). eapply eval_divlu_base; eauto.
+  destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS. 
+** destruct x; simpl in H1; try discriminate.
+   destruct (Int64.eq n2 Int64.zero); inv H1.
+   econstructor; split; eauto. econstructor. eauto. eapply eval_divlu_mull; eauto.  
+** eapply eval_divlu_base; eauto.     
 - eapply eval_divlu_base; eauto.
 Qed.
 
@@ -595,10 +775,56 @@ Proof.
   econstructor; split. apply eval_longconst. constructor.
 + destruct (Int64.is_power2 n2) as [l|] eqn:POW.
 * exploit Val.modlu_pow2; eauto. intros EQ; subst z. eapply eval_andl; eauto. apply eval_longconst.
-* eapply eval_modlu_base; eauto.     
+* destruct (Compopts.optim_for_size tt). eapply eval_modlu_base; eauto.
+  destruct (divlu_mul_params (Int64.unsigned n2)) as [[p M]|] eqn:PARAMS. 
+** destruct x; simpl in H1; try discriminate.
+   destruct (Int64.eq n2 Int64.zero) eqn:Z; inv H1.
+   rewrite Int64.modu_divu. 
+    econstructor; split; eauto. econstructor. eauto.
+    eapply eval_modl_from_divl; eauto.  
+    eapply eval_divlu_mull; eauto.
+    red; intros; subst n2; discriminate Z.  
+** eapply eval_modlu_base; eauto.     
 - eapply eval_modlu_base; eauto.
 Qed.
 
+Lemma eval_divls_mull:
+  forall le x y p M,
+  divls_mul_params (Int64.signed y) = Some(p, M) ->
+  nth_error le O = Some (Vlong x) ->
+  eval_expr ge sp e m le (divls_mull p M) (Vlong (Int64.divs x y)).
+Proof.
+  intros. unfold divls_mull.
+  assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)).
+  { constructor; auto. }
+  exploit eval_mullhs. eauto. eexact A0. instantiate (1 := Int64.repr M).  intros (v1 & A1 & B1).
+  exploit eval_addl. eexact A1. eexact A0. intros (v2 & A2 & B2).
+  exploit eval_shrluimm. eauto. eexact A0. instantiate (1 := Int.repr 63). intros (v3 & A3 & B3).
+  set (a4 := if zlt M Int64.half_modulus
+             then mullhs (Eletvar 0) (Int64.repr M)
+             else addl (mullhs (Eletvar 0) (Int64.repr M)) (Eletvar 0)).
+  set (v4 := if zlt M Int64.half_modulus then v1 else v2).
+  assert (A4: eval_expr ge sp e m le a4 v4). 
+  { unfold a4, v4; destruct (zlt M Int64.half_modulus); auto. }
+  exploit eval_shrlimm. eauto. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5).
+  exploit eval_addl. eexact A5. eexact A3. intros (v6 & A6 & B6).
+  assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true).
+  { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto.
+    assert (64 < Int.max_unsigned) by (compute; auto). omega. }
+  simpl in B1; inv B1.
+  simpl in B2; inv B2.
+  simpl in B3; rewrite RANGE in B3 by omega; inv B3.
+  destruct (zlt M Int64.half_modulus).
+- exploit (divls_mul_shift_1 x); eauto. intros [A B].
+  simpl in B5; rewrite RANGE in B5 by auto; inv B5.
+  simpl in B6; inv B6. 
+  rewrite B; exact A6.
+- exploit (divls_mul_shift_2 x); eauto. intros [A B].
+  simpl in B5; rewrite RANGE in B5 by auto; inv B5.
+  simpl in B6; inv B6. 
+  rewrite B; exact A6.
+Qed.
+
 Theorem eval_divls:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
@@ -618,8 +844,15 @@ Proof.
 + destruct (Int64.is_power2' n2) as [l|] eqn:POW.
 * destruct (Int.ltu l (Int.repr 63)) eqn:LT.
 ** exploit Val.divls_pow2; eauto. intros EQ. eapply eval_shrxlimm; eauto.
-** eapply eval_divls_base; eauto.  
-* eapply eval_divls_base; eauto.     
+** eapply eval_divls_base; eauto.
+* destruct (Compopts.optim_for_size tt). eapply eval_divls_base; eauto.
+  destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS. 
+** destruct x; simpl in H1; try discriminate.
+   destruct (Int64.eq n2 Int64.zero
+             || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1.
+   econstructor; split; eauto. econstructor. eauto.
+   eapply eval_divls_mull; eauto.
+** eapply eval_divls_base; eauto.
 - eapply eval_divls_base; eauto.
 Qed.
 
@@ -654,7 +887,16 @@ Proof.
   econstructor. eauto. eapply eval_modl_from_divl. eexact A1. reflexivity.      
   rewrite Int64.mods_divs. auto.
 **eapply eval_modls_base; eauto.
-* eapply eval_modls_base; eauto.     
+* destruct (Compopts.optim_for_size tt). eapply eval_modls_base; eauto.
+  destruct (divls_mul_params (Int64.signed n2)) as [[p M]|] eqn:PARAMS. 
+** destruct x; simpl in H1; try discriminate.
+   destruct (Int64.eq n2 Int64.zero
+             || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1.
+   econstructor; split; eauto. econstructor. eauto.
+   rewrite Int64.mods_divs. 
+   eapply eval_modl_from_divl; auto.
+   eapply eval_divls_mull; eauto.
+** eapply eval_modls_base; eauto.     
 - eapply eval_modls_base; eauto.
 Qed.
 
diff --git a/backend/Selection.v b/backend/Selection.v
index 5cb5d119..abda1d95 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -389,10 +389,13 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions :=
   do i64_shl <- lookup_helper globs "__i64_shl" sig_li_l ;
   do i64_shr <- lookup_helper globs "__i64_shr" sig_li_l ;
   do i64_sar <- lookup_helper globs "__i64_sar" sig_li_l ;
+  do i64_umulh <- lookup_helper globs "__i64_umulh" sig_ll_l ;
+  do i64_smulh <- lookup_helper globs "__i64_smulh" sig_ll_l ;
   OK (mk_helper_functions
      i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof
      i64_sdiv i64_udiv i64_smod i64_umod
-     i64_shl i64_shr i64_sar).
+     i64_shl i64_shr i64_sar
+     i64_umulh i64_smulh).
 
 (** Conversion of programs. *)
 
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index 5891adef..f7eeebd0 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -38,7 +38,9 @@ Class helper_functions := mk_helper_functions {
   i64_umod: ident;                      (**r unsigned remainder *)
   i64_shl: ident;                       (**r shift left *)
   i64_shr: ident;                       (**r shift right unsigned *)
-  i64_sar: ident                        (**r shift right signed *)
+  i64_sar: ident;                       (**r shift right signed *)
+  i64_umulh: ident;                     (**r unsigned multiply high *)
+  i64_smulh: ident;                     (**r signed multiply high *)
 }.
 
 Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
@@ -255,6 +257,11 @@ Definition mull (e1 e2: expr) :=
   | _, _ => mull_base e1 e2
   end.
 
+Definition mullhu (e1: expr) (n2: int64) :=
+  Eexternal i64_umulh sig_ll_l (e1 ::: longconst n2 ::: Enil).
+Definition mullhs (e1: expr) (n2: int64) :=
+  Eexternal i64_smulh sig_ll_l (e1 ::: longconst n2 ::: Enil).
+
 Definition shrxlimm (e: expr) (n: int) :=
   if Int.eq n Int.zero then e else
     Elet e (shrlimm (addl (Eletvar O)
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index a10ee3f7..31f5db67 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -48,7 +48,9 @@ Axiom i64_helpers_correct :
  /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__i64_umod" sig_ll_l (x::y::nil) z)
  /\ (forall x y, external_implements "__i64_shl" sig_li_l (x::y::nil) (Val.shll x y))
  /\ (forall x y, external_implements "__i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
- /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)).
+ /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl x y))
+ /\ (forall x y, external_implements "__i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y))
+ /\ (forall x y, external_implements "__i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)).
 
 Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
   (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))).
@@ -66,7 +68,9 @@ Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F)
   /\ helper_declared p i64_umod "__i64_umod" sig_ll_l
   /\ helper_declared p i64_shl "__i64_shl" sig_li_l
   /\ helper_declared p i64_shr "__i64_shr" sig_li_l
-  /\ helper_declared p i64_sar "__i64_sar" sig_li_l.
+  /\ helper_declared p i64_sar "__i64_sar" sig_li_l
+  /\ helper_declared p i64_umulh "__i64_umulh" sig_ll_l
+  /\ helper_declared p i64_smulh "__i64_smulh" sig_ll_l.
 
 (** * Correctness of the instruction selection functions for 64-bit operators *)
 
@@ -823,6 +827,20 @@ Proof.
 - apply eval_mull_base; auto.
 Qed.
 
+Theorem eval_mullhu: 
+  forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)).
+Proof.
+  unfold mullhu; intros; red; intros. econstructor; split; eauto. 
+  eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. 
+Qed.
+
+Theorem eval_mullhs: 
+  forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)).
+Proof.
+  unfold mullhs; intros; red; intros. econstructor; split; eauto. 
+  eapply eval_helper_2; eauto. apply eval_longconst. DeclHelper; eauto. UseHelper. 
+Qed.
+
 Theorem eval_shrxlimm:
   forall le a n x z,
   Archi.ptr64 = false ->
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index bf88a450..be8bcccc 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1866,6 +1866,18 @@ Lemma mull_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mull v w) (mull x y).
 Proof (binop_long_sound Int64.mul).
 
+Definition mullhs := binop_long Int64.mulhs.
+
+Lemma mullhs_sound:
+  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mullhs v w) (mullhs x y).
+Proof (binop_long_sound Int64.mulhs).
+
+Definition mullhu := binop_long Int64.mulhu.
+
+Lemma mullhu_sound:
+  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mullhu v w) (mullhu x y).
+Proof (binop_long_sound Int64.mulhu).
+
 Definition divls (v w: aval) :=
   match w, v with
   | L i2, L i1 =>
@@ -4559,7 +4571,8 @@ Hint Resolve cnot_sound symbol_address_sound
        divs_sound divu_sound mods_sound modu_sound shrx_sound
        shll_sound shrl_sound shrlu_sound
        andl_sound orl_sound xorl_sound notl_sound roll_sound rorl_sound
-       negl_sound addl_sound subl_sound mull_sound
+       negl_sound addl_sound subl_sound
+       mull_sound mullhs_sound mullhu_sound
        divls_sound divlu_sound modls_sound modlu_sound shrxl_sound
        negf_sound absf_sound
        addf_sound subf_sound mulf_sound divf_sound
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index b68887c5..38ef45e7 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -251,6 +251,14 @@ let builtins_generic = {
     "__i64_sar",
         (TInt(ILongLong, []),
          [TInt(ILongLong, []); TInt(IInt, [])],
+         false);
+    "__i64_smulh",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(ILongLong, [])],
+         false);
+    "__i64_umulh",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IULongLong, [])],
          false)
   ]
 }
diff --git a/common/Values.v b/common/Values.v
index 88506bab..cfabb7a5 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -622,6 +622,18 @@ Definition mull' (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
+Definition mullhs (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.mulhs n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition mullhu (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.mulhu n1 n2)
+  | _, _ => Vundef
+  end.
+
 Definition divls (v1 v2: val): option val :=
   match v1, v2 with
   | Vlong n1, Vlong n2 =>
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 01ecb15a..9d4036ff 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -164,9 +164,9 @@ Inductive instruction: Type :=
   | Pimull_ri (rd: ireg) (n: int)
   | Pimulq_ri (rd: ireg) (n: int64)
   | Pimull_r (r1: ireg)
-(*  | Pimulq_r (r1: ireg) *)
+  | Pimulq_r (r1: ireg)
   | Pmull_r (r1: ireg)
-(*  | Pmulq_r (r1: ireg) *)
+  | Pmulq_r (r1: ireg)
   | Pcltd
   | Pcqto
   | Pdivl (r1: ireg)
@@ -718,9 +718,15 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pimull_r r1 =>
       Next (nextinstr_nf (rs#RAX <- (Val.mul rs#RAX rs#r1)
                             #RDX <- (Val.mulhs rs#RAX rs#r1))) m
+  | Pimulq_r r1 =>
+      Next (nextinstr_nf (rs#RAX <- (Val.mull rs#RAX rs#r1)
+                            #RDX <- (Val.mullhs rs#RAX rs#r1))) m
   | Pmull_r r1 =>
       Next (nextinstr_nf (rs#RAX <- (Val.mul rs#RAX rs#r1)
                             #RDX <- (Val.mulhu rs#RAX rs#r1))) m
+  | Pmulq_r r1 =>
+      Next (nextinstr_nf (rs#RAX <- (Val.mull rs#RAX rs#r1)
+                            #RDX <- (Val.mullhu rs#RAX rs#r1))) m
   | Pcltd =>
       Next (nextinstr_nf (rs#RDX <- (Val.shr rs#RAX (Vint (Int.repr 31))))) m
   | Pcqto =>
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index ccf2e6fd..bb26d507 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -453,6 +453,14 @@ Definition transl_op
   | Omullimm n, a1 :: nil =>
       assertion (mreg_eq a1 res);
       do r <- ireg_of res; OK (Pimulq_ri r n :: k)
+  | Omullhs, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 AX);
+      assertion (mreg_eq res DX);
+      do r2 <- ireg_of a2; OK (Pimulq_r r2 :: k)
+  | Omullhu, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 AX);
+      assertion (mreg_eq res DX);
+      do r2 <- ireg_of a2; OK (Pmulq_r r2 :: k)
   | Odivl, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 AX);
       assertion (mreg_eq a2 CX);
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 4effe7c9..05b3176a 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -1312,6 +1312,10 @@ Transparent destroyed_by_op.
 (* lea *)
   exploit transl_addressing_mode_32_correct; eauto. intros EA.
   TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss. rewrite normalize_addrmode_32_correct; auto.
+(* mullhs *)
+  apply SAME. TranslOp. destruct H1. Simplifs.
+(* mullhu *)
+  apply SAME. TranslOp. destruct H1. Simplifs.
 (* divl *)
   apply SAME.
   exploit (divls_modls_exists (rs RAX) (rs RCX)). left; congruence.
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index a9383d18..034fa4bb 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -133,6 +133,8 @@ Definition destroyed_by_op (op: operation): list mreg :=
   | Omod => AX :: DX :: nil
   | Omodu => AX :: DX :: nil
   | Oshrximm _ => CX :: nil
+  | Omullhs => AX :: DX :: nil
+  | Omullhu => AX :: DX :: nil
   | Odivl => AX :: DX :: nil
   | Odivlu => AX :: DX :: nil
   | Omodl => AX :: DX :: nil
@@ -211,6 +213,8 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg
   | Oshr => (None :: Some CX :: nil, None)
   | Oshru => (None :: Some CX :: nil, None)
   | Oshrximm _ => (Some AX :: nil, Some AX)
+  | Omullhs => (Some AX :: None :: nil, Some DX)
+  | Omullhu => (Some AX :: None :: nil, Some DX)
   | Odivl => (Some AX :: Some CX :: nil, Some AX)
   | Odivlu => (Some AX :: Some CX :: nil, Some AX)
   | Omodl => (Some AX :: Some CX :: nil, Some DX)
@@ -300,6 +304,8 @@ Definition two_address_op (op: operation) : bool :=
   | Osubl => true
   | Omull => true
   | Omullimm _ => true
+  | Omullhs => false
+  | Omullhu => false
   | Odivl => false
   | Odivlu => false
   | Omodl => false
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v
index 575532b1..09013cdd 100644
--- a/ia32/NeedOp.v
+++ b/ia32/NeedOp.v
@@ -95,10 +95,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Osubl => op2 (default nv)
   | Omull => op2 (default nv)
   | Omullimm _ => op1 (default nv)
-  | Odivl => op2 (default nv)
-  | Odivlu => op2 (default nv)
-  | Omodl => op2 (default nv)
-  | Omodlu => op2 (default nv)
+  | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv)
   | Oandl => op2 (default nv)
   | Oandlimm _ => op1 (default nv)
   | Oorl => op2 (default nv)
diff --git a/ia32/Op.v b/ia32/Op.v
index 1d0e8472..eb2fd110 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -120,6 +120,8 @@ Inductive operation : Type :=
   | Osubl                    (**r [rd = r1 - r2] *)
   | Omull                    (**r [rd = r1 * r2] *)
   | Omullimm (n: int64)      (**r [rd = r1 * n] *)
+  | Omullhs                  (**r [rd = high part of r1 * r2, signed] *)
+  | Omullhu                  (**r [rd = high part of r1 * r2, unsigned] *)
   | Odivl                    (**r [rd = r1 / r2] (signed) *)
   | Odivlu                   (**r [rd = r1 / r2] (unsigned) *)
   | Omodl                    (**r [rd = r1 % r2] (signed) *)
@@ -339,6 +341,8 @@ Definition eval_operation
   | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
   | Omull, v1::v2::nil => Some (Val.mull v1 v2)
   | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n))
+  | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2)
+  | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2)
   | Odivl, v1::v2::nil => Val.divls v1 v2
   | Odivlu, v1::v2::nil => Val.divlu v1 v2
   | Omodl, v1::v2::nil => Val.modls v1 v2
@@ -508,6 +512,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubl => (Tlong :: Tlong :: nil, Tlong)
   | Omull => (Tlong :: Tlong :: nil, Tlong)
   | Omullimm _ => (Tlong :: nil, Tlong)
+  | Omullhs => (Tlong :: Tlong :: nil, Tlong)
+  | Omullhu => (Tlong :: Tlong :: nil, Tlong)
   | Odivl => (Tlong :: Tlong :: nil, Tlong)
   | Odivlu => (Tlong :: Tlong :: nil, Tlong)
   | Omodl => (Tlong :: Tlong :: nil, Tlong)
@@ -666,6 +672,8 @@ Proof with (try exact I).
     unfold Val.has_type; destruct Archi.ptr64; simpl; auto. destruct (eq_block b b0); auto.
   destruct v0; destruct v1...
   destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
   destruct v0; destruct v1; simpl in *; inv H0.
     destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
   destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2...
@@ -1210,6 +1218,8 @@ Proof.
   apply Val.subl_inject; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl.
     destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl.
diff --git a/ia32/PrintOp.ml b/ia32/PrintOp.ml
index b6147197..faa5bb5f 100644
--- a/ia32/PrintOp.ml
+++ b/ia32/PrintOp.ml
@@ -109,7 +109,7 @@ let print_operation reg pp = function
   | Oshruimm n, [r1] -> fprintf pp "%a >>u %ld" reg r1 (camlint_of_coqint n)
   | Ororimm n, [r1] -> fprintf pp "%a ror %ld" reg r1 (camlint_of_coqint n)
   | Oshldimm n, [r1;r2] -> fprintf pp "(%a, %a) << %ld" reg r1 reg r2 (camlint_of_coqint n)
-  | Olea addr, args -> print_addressing reg pp (addr, args); fprintf pp " (lea)"
+  | Olea addr, args -> print_addressing reg pp (addr, args); fprintf pp " (int)"
   | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
   | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1
   | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1
@@ -119,6 +119,8 @@ let print_operation reg pp = function
   | Osubl, [r1;r2] -> fprintf pp "%a -l %a" reg r1 reg r2
   | Omull, [r1;r2] -> fprintf pp "%a *l %a" reg r1 reg r2
   | Omullimm n, [r1] -> fprintf pp "%a *l %Ld" reg r1 (camlint64_of_coqint n)
+  | Omullhs, [r1;r2] -> fprintf pp "mullhs(%a,%a)" reg r1 reg r2
+  | Omullhu, [r1;r2] -> fprintf pp "mullhu(%a,%a)" reg r1 reg r2
   | Odivl, [r1;r2] -> fprintf pp "%a /ls %a" reg r1 reg r2
   | Odivlu, [r1;r2] -> fprintf pp "%a /lu %a" reg r1 reg r2
   | Omodl, [r1;r2] -> fprintf pp "%a %%ls %a" reg r1 reg r2
@@ -138,7 +140,7 @@ let print_operation reg pp = function
   | Oshrlu, [r1;r2] -> fprintf pp "%a >>lu %a" reg r1 reg r2
   | Oshrluimm n, [r1] -> fprintf pp "%a >>lu %ld" reg r1 (camlint_of_coqint n)
   | Ororlimm n, [r1] -> fprintf pp "%a rorl %ld" reg r1 (camlint_of_coqint n)
-  | Oleal addr, args -> print_addressing reg pp (addr, args); fprintf pp " (leal)"
+  | Oleal addr, args -> print_addressing reg pp (addr, args); fprintf pp " (long)"
   | Onegf, [r1] -> fprintf pp "negf(%a)" reg r1
   | Oabsf, [r1] -> fprintf pp "absf(%a)" reg r1
   | Oaddf, [r1;r2] -> fprintf pp "%a +f %a" reg r1 reg r2
diff --git a/ia32/SelectLong.vp b/ia32/SelectLong.vp
index 77fc4071..2869f823 100644
--- a/ia32/SelectLong.vp
+++ b/ia32/SelectLong.vp
@@ -285,6 +285,14 @@ Nondetfunction mull (e1: expr) (e2: expr) :=
   | _, _ => Eop Omull (e1:::e2:::Enil)
   end.
 
+Definition mullhu (e1: expr) (n2: int64) :=
+  if Archi.splitlong then SplitLong.mullhu e1 n2 else
+  Eop Omullhu (e1 ::: longconst n2 ::: Enil).
+
+Definition mullhs (e1: expr) (n2: int64) :=
+  if Archi.splitlong then SplitLong.mullhs e1 n2 else
+  Eop Omullhs (e1 ::: longconst n2 ::: Enil).
+
 Definition shrxlimm (e: expr) (n: int) :=
   if Archi.splitlong then SplitLong.shrxlimm e n else
   if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil).
diff --git a/ia32/SelectLongproof.v b/ia32/SelectLongproof.v
index 4cd15fd3..14b0bcce 100644
--- a/ia32/SelectLongproof.v
+++ b/ia32/SelectLongproof.v
@@ -428,6 +428,20 @@ Proof.
 - TrivialExists.
 Qed.
 
+Theorem eval_mullhu: 
+  forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)).
+Proof.
+  unfold mullhu; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhu; auto.
+  red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto.
+Qed.
+
+Theorem eval_mullhs: 
+  forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)).
+Proof.
+  unfold mullhs; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhs; auto.
+  red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto.
+Qed.
+
 Theorem eval_shrxlimm:
   forall le a n x z,
   eval_expr ge sp e m le a x ->
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index c3e70042..fbc219d1 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -438,8 +438,12 @@ module Target(System: SYSTEM):TARGET =
           fprintf oc "	imulq	%a, %a\n" intconst64 n ireg64 rd
       | Pimull_r(r1) ->
           fprintf oc "	imull	%a\n" ireg32 r1
+      | Pimulq_r(r1) ->
+          fprintf oc "	imulq	%a\n" ireg64 r1
       | Pmull_r(r1) ->
           fprintf oc "	mull	%a\n" ireg32 r1
+      | Pmulq_r(r1) ->
+          fprintf oc "	mulq	%a\n" ireg64 r1
       | Pcltd ->
           fprintf oc "	cltd\n"
       | Pcqto ->
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index c8b3278e..98f0dbb1 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -117,6 +117,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osubl, v1::v2::nil => subl v1 v2
   | Omull, v1::v2::nil => mull v1 v2
   | Omullimm n, v1::nil => mull v1 (L n)
+  | Omullhs, v1::v2::nil => mullhs v1 v2
+  | Omullhu, v1::v2::nil => mullhu v1 v2
   | Odivl, v1::v2::nil => divls v1 v2
   | Odivlu, v1::v2::nil => divlu v1 v2
   | Omodl, v1::v2::nil => modls v1 v2
diff --git a/runtime/Makefile b/runtime/Makefile
index 59d2bb64..b94db3ca 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -14,6 +14,7 @@ else
 OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
   i64_shr.o i64_smod.o i64_stod.o i64_stof.o \
   i64_udivmod.o i64_udiv.o i64_umod.o i64_utod.o i64_utof.o \
+  i64_smulh.o i64_umulh.o \
   vararg.o
 endif
 
diff --git a/runtime/c/i64.h b/runtime/c/i64.h
index dd584533..a75214fe 100644
--- a/runtime/c/i64.h
+++ b/runtime/c/i64.h
@@ -41,3 +41,5 @@ extern signed long long __i64_sar(signed long long x, int amount);
 extern unsigned long long __i64_udivmod(unsigned long long n,
                                         unsigned long long d,
                                         unsigned long long * rp);
+extern unsigned long long __i64_umulh(unsigned long long u,
+                                      unsigned long long v);
diff --git a/runtime/c/i64_smulh.c b/runtime/c/i64_smulh.c
new file mode 100644
index 00000000..b7a42474
--- /dev/null
+++ b/runtime/c/i64_smulh.c
@@ -0,0 +1,56 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris-Rocquencourt
+ *
+ * Copyright (c) 2013 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+typedef signed long long s64;
+typedef unsigned long long u64;
+
+/* Signed multiply high */
+
+/* Hacker's Delight section 8.3:
+ * - compute high 64 bits of the unsigned product X * Y
+ * - subtract X if Y < 0
+ * - subtract Y if X < 0 
+ */
+
+s64 __i64_smulh(s64 x, s64 y)
+{
+  s64 t = (s64) __i64_umulh(x, y);
+  if (y < 0) t = t - x;
+  if (x < 0) t = t - y;
+  return t;
+}
diff --git a/runtime/c/i64_umulh.c b/runtime/c/i64_umulh.c
new file mode 100644
index 00000000..d2394d09
--- /dev/null
+++ b/runtime/c/i64_umulh.c
@@ -0,0 +1,66 @@
+/*****************************************************************
+ *
+ *               The Compcert verified compiler
+ *
+ *           Xavier Leroy, INRIA Paris
+ *
+ * Copyright (c) 2016 Institut National de Recherche en Informatique et
+ *  en Automatique.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of the <organization> nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+ * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ **********************************************************************/
+
+/* Helper functions for 64-bit integer arithmetic. Reference C implementation */
+
+#include "i64.h"
+
+typedef unsigned long long u64;
+typedef unsigned int u32;
+
+/* Unsigned multiply high */
+
+/* Hacker's Delight, algorithm 8.1, specialized to two 32-bit words */
+
+u64 __i64_umulh(u64 u, u64 v)
+{
+  u32 u0 = u, u1 = u >> 32;
+  u32 v0 = v, v1 = v >> 32;
+  u32 w1, w2, w3, k;
+  u64 t;
+
+  t = (u64) u0 * (u64) v0;
+  k = t >> 32;
+
+  t = (u64) u1 * (u64) v0 + k;
+  w1 = t;
+  w2 = t >> 32;
+
+  t = (u64) u0 * (u64) v1 + w1;
+  k = t >> 32;
+
+  t = (u64) u1 * (u64) v1 + w2 + k;
+
+  return t;
+}
diff --git a/runtime/ia32/i64_smulh.S b/runtime/ia32/i64_smulh.S
new file mode 100644
index 00000000..cc0f0167
--- /dev/null
+++ b/runtime/ia32/i64_smulh.S
@@ -0,0 +1,94 @@
+// *****************************************************************
+//
+//               The Compcert verified compiler
+//
+//           Xavier Leroy, INRIA Paris
+//
+// Copyright (c) 2016 Institut National de Recherche en Informatique et
+//  en Automatique.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//     * Redistributions of source code must retain the above copyright
+//       notice, this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//     * Neither the name of the <organization> nor the
+//       names of its contributors may be used to endorse or promote products
+//       derived from this software without specific prior written permission.
+// 
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+//
+// *********************************************************************
+
+// Helper functions for 64-bit integer arithmetic.  IA32 version.
+	
+#include "sysdeps.h"
+
+// Multiply-high signed
+
+#define XL 12(%esp)
+#define XH 16(%esp)
+#define YL 20(%esp)
+#define YH 24(%esp)
+
+// Hacker's Delight section 8.3:
+// - compute high 64 bits of the unsigned product X * Y  (see i64_umulh.S)
+// - subtract X if Y < 0
+// - subtract Y if X < 0
+
+FUNCTION(__i64_smulh)
+        pushl %esi
+        pushl %edi
+	movl XL, %eax
+        mull YL                 // EDX:EAX = 64-bit product XL.YL
+        movl %edx, %ecx
+        xorl %esi, %esi
+        xorl %edi, %edi         // EDI:ESI:ECX accumulatesbits 127:32 of result
+        movl XH, %eax
+        mull YL                 // EDX:EAX = 64-bit product XH.YL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl YH, %eax
+        mull XL                 // EDX:EAX = 64-bit product YH.XL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl XH, %eax
+        mull YH                 // EDX:EAX = 64-bit product XH.YH
+	addl %eax, %esi
+        adcl %edx, %edi
+// Here, EDI:ESI is the high 64 bits of the unsigned product X.Y
+        xorl %eax, %eax
+        xorl %edx, %edx
+        cmpl $0, XH
+        cmovl YL, %eax
+        cmovl YH, %edx          // EDX:EAX = Y if X < 0, = 0 if X >= 0
+        subl %eax, %esi
+        sbbl %edx, %edi         // EDI:ESI -= Y  if X < 0
+        xorl %eax, %eax
+        xorl %edx, %edx
+        cmpl $0, YH
+        cmovl XL, %eax
+        cmovl XH, %edx          // EDX:EAX = X if Y < 0, = 0 if Y >= 0
+        subl %eax, %esi
+        sbbl %edx, %edi         // EDI:ESI -= X  if Y < 0
+// Now EDI:ESI contains the high 64 bits of the signed product X.Y
+        movl %esi, %eax
+        movl %edi, %edx
+        popl %edi
+        popl %esi
+        ret
+ENDFUNCTION(__i64_smulh)
diff --git a/runtime/ia32/i64_umulh.S b/runtime/ia32/i64_umulh.S
new file mode 100644
index 00000000..449a0f8b
--- /dev/null
+++ b/runtime/ia32/i64_umulh.S
@@ -0,0 +1,74 @@
+// *****************************************************************
+//
+//               The Compcert verified compiler
+//
+//           Xavier Leroy, INRIA Paris
+//
+// Copyright (c) 2016 Institut National de Recherche en Informatique et
+//  en Automatique.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//     * Redistributions of source code must retain the above copyright
+//       notice, this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//     * Neither the name of the <organization> nor the
+//       names of its contributors may be used to endorse or promote products
+//       derived from this software without specific prior written permission.
+// 
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+//
+// *********************************************************************
+
+// Helper functions for 64-bit integer arithmetic.  IA32 version.
+	
+#include "sysdeps.h"
+
+// Multiply-high unsigned
+
+#define XL 12(%esp)
+#define XH 16(%esp)
+#define YL 20(%esp)
+#define YH 24(%esp)
+
+// X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL
+
+FUNCTION(__i64_umulh)
+        pushl %esi
+        pushl %edi
+	movl XL, %eax
+        mull YL                 // EDX:EAX = 64-bit product XL.YL
+        movl %edx, %ecx
+        xorl %esi, %esi
+        xorl %edi, %edi         // EDI:ESI:ECX accumulate bits 127:32 of result
+        movl XH, %eax
+        mull YL                 // EDX:EAX = 64-bit product XH.YL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl YH, %eax
+        mull XL                 // EDX:EAX = 64-bit product YH.XL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl XH, %eax
+        mull YH                 // EDX:EAX = 64-bit product XH.YH
+	addl %esi, %eax
+        adcl %edi, %edx
+	popl %edi
+	popl %esi
+        ret
+ENDFUNCTION(__i64_umulh)
+
diff --git a/runtime/powerpc/i64_smul.s b/runtime/powerpc/i64_smul.s
new file mode 100644
index 00000000..9eb453d4
--- /dev/null
+++ b/runtime/powerpc/i64_smul.s
@@ -0,0 +1,76 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris
+#
+# Copyright (c) 2016 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+# Signed multiply high
+	
+# Reference C implementation in ../c/i64_smul.c
+
+        .balign 16
+        .globl __i64_smulh
+__i64_smulh:
+     # u1 in r3; u0 in r4; v1 in r5; v0 in r6
+     # First compute unsigned product (see i64_umul.s)
+        mulhwu   r0, r4, r6     # k (in r0) = high((u64) u0 * (u64) v0)
+        mullw    r8, r3, r6
+        mulhwu   r7, r3, r6     # t (in r8:r7) = (u64) u1 * (u64) v0
+        addc     r0, r8, r0     # w1 (in r0) = low (t + k)
+        addze    r9, r7         # w2 (in r9) = high (t + k)
+        mullw    r8, r4, r5
+        mulhwu   r7, r4, r5     # t (in r8:r7) = (u64) u0 * (u64) v1
+        addc     r0, r8, r0     # tmp (in r0) = low (t + w1)
+        addze    r0, r7         # k (in r0) = high(t + w1)
+        mullw    r8, r3, r5
+        mulhwu   r7, r3, r5     # t (in r8:r7) = (u64) u1 * (u64) v1
+        addc     r8, r8, r9     # add w2
+        addze    r7, r7
+        addc     r8, r8, r0     # add k
+        addze    r7, r7
+     # Here r8:r7 contains the high 64 bits of the unsigned product
+        srawi    r0, r3, 31     # r0 = 0 if U >= 0, -1 if U < 0
+        srawi    r9, r5, 31     # r9 = 0 if V >= 0, -1 if V < 0
+        and      r3, r3, r9
+        and      r4, r4, r9     # r3:r4 = U if V < 0, = 0 if V >= 0
+        and      r5, r5, r0
+        and      r6, r6, r0     # r5:r6 = V if U < 0, = 0 if U >= 0
+        subfc    r8, r4, r8
+        subfe    r7, r3, r7
+        subfc    r4, r6, r8
+        subfe    r3, r5, r7     # result is r8:r7 - r3:r4 - r5:r6
+        blr
+        .type __i64_umulh, @function
+        .size __i64_umulh, .-__i64_umulh
diff --git a/runtime/powerpc/i64_umul.s b/runtime/powerpc/i64_umul.s
new file mode 100644
index 00000000..e734b93c
--- /dev/null
+++ b/runtime/powerpc/i64_umul.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris
+#
+# Copyright (c) 2016 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+# Unsigned multiply high
+	
+# Reference C implementation in ../c/i64_umul.c
+
+        .balign 16
+        .globl __i64_umulh
+__i64_umulh:
+     # u1 in r3; u0 in r4; v1 in r5; v0 in r6
+        mulhwu   r0, r4, r6     # k (in r0) = high((u64) u0 * (u64) v0)
+        mullw    r8, r3, r6
+        mulhwu   r7, r3, r6     # t (in r8:r7) = (u64) u1 * (u64) v0
+        addc     r0, r8, r0     # w1 (in r0) = low (t + k)
+        addze    r9, r7         # w2 (in r9) = high (t + k)
+        mullw    r8, r4, r5
+        mulhwu   r7, r4, r5     # t (in r8:r7) = (u64) u0 * (u64) v1
+        addc     r0, r8, r0     # tmp (in r0) = low (t + w1)
+        addze    r0, r7         # k (in r0) = high(t + w1)
+        mullw    r8, r3, r5
+        mulhwu   r7, r3, r5     # t (in r8:r7) = (u64) u1 * (u64) v1
+        addc     r4, r8, r9     # add w2
+        addze    r3, r7
+        addc     r4, r4, r0     # add k
+        addze    r3, r3
+        blr
+        .type __i64_umulh, @function
+        .size __i64_umulh, .-__i64_umulh
diff --git a/test/regression/Results/int64 b/test/regression/Results/int64
index 307d0887..af444cf6 100644
--- a/test/regression/Results/int64
+++ b/test/regression/Results/int64
@@ -12,6 +12,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 0
@@ -42,6 +54,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 1
@@ -72,6 +96,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = ffffffffffffffff
@@ -102,6 +138,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 7fffffff
@@ -132,6 +180,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 80000000
@@ -162,6 +222,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 7fffffffffffffff
@@ -192,6 +264,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 8000000000000000
@@ -222,6 +306,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 100000003
@@ -252,6 +348,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = 0
+x /u 5 = 0
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = 0
+x /u 11 = 0
+x %u 11 = 0
+x /s 11 = 0
+x %s 11 = 0
 ~x = ffffffffffffffff
 x & y = 0
 x | y = 14057b7ef767814f
@@ -282,6 +390,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 8ada4b0819379bb
+x %u 3 = 1
+x /s 3 = 8ada4b0819379bb
+x %s 3 = 1
+x /u 5 = 534fc69e7587c3d
+x %u 5 = 1
+x /s 5 = 534fc69e7587c3d
+x %s 5 = 1
+x /u 11 = 25de718dd854fbe
+x %u 11 = 8
+x /s 11 = 25de718dd854fbe
+x %s 11 = 8
 ~x = e5f711ee7b4592cd
 x & y = 0
 x | y = 1a08ee1184ba6d32
@@ -312,6 +432,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 0
 x | y = 1
@@ -342,6 +474,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 1
 x | y = 1
@@ -372,6 +516,18 @@ x /u y2 = 0
 x %u y2 = 1
 x /s y3 = ffffffffffffffff
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 1
 x | y = ffffffffffffffff
@@ -402,6 +558,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 1
 x | y = 7fffffff
@@ -432,6 +600,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 0
 x | y = 80000001
@@ -462,6 +642,18 @@ x /u y2 = 0
 x %u y2 = 1
 x /s y3 = 0
 x %s y3 = 1
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 1
 x | y = 7fffffffffffffff
@@ -492,6 +684,18 @@ x /u y2 = 0
 x %u y2 = 1
 x /s y3 = 0
 x %s y3 = 1
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 0
 x | y = 8000000000000001
@@ -522,6 +726,18 @@ x /u y2 = 1
 x %u y2 = 0
 x /s y3 = 1
 x %s y3 = 0
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 1
 x | y = 100000003
@@ -552,6 +768,18 @@ x /u y2 = 0
 x %u y2 = 1
 x /s y3 = 0
 x %s y3 = 1
+x /u 3 = 0
+x %u 3 = 1
+x /s 3 = 0
+x %s 3 = 1
+x /u 5 = 0
+x %u 5 = 1
+x /s 5 = 0
+x %s 5 = 1
+x /u 11 = 0
+x %u 11 = 1
+x /s 11 = 0
+x %s 11 = 1
 ~x = fffffffffffffffe
 x & y = 1
 x | y = 9af678222e728119
@@ -582,6 +810,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 223cb3a32a60333c
+x %u 3 = 0
+x /s 3 = 223cb3a32a60333c
+x %s 3 = 0
+x /u 5 = 148ad22eb3068524
+x %u 5 = 0
+x /s 5 = 148ad22eb3068524
+x %s 5 = 0
+x /u 11 = 9565f8997318256
+x %u 11 = 2
+x /s 11 = 9565f8997318256
+x %s 11 = 2
 ~x = 9949e51680df664b
 x & y = 0
 x | y = 66b61ae97f2099b5
@@ -612,6 +852,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 0
 x | y = ffffffffffffffff
@@ -642,6 +894,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 1
 x | y = ffffffffffffffff
@@ -672,6 +936,18 @@ x /u y2 = 100000001
 x %u y2 = 0
 x /s y3 = 1
 x %s y3 = 0
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = ffffffffffffffff
 x | y = ffffffffffffffff
@@ -702,6 +978,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 7fffffff
 x | y = ffffffffffffffff
@@ -732,6 +1020,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 80000000
 x | y = ffffffffffffffff
@@ -762,6 +1062,18 @@ x /u y2 = 200000004
 x %u y2 = 3
 x /s y3 = 0
 x %s y3 = ffffffffffffffff
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 7fffffffffffffff
 x | y = ffffffffffffffff
@@ -792,6 +1104,18 @@ x /u y2 = 1ffffffff
 x %u y2 = 7fffffff
 x /s y3 = 0
 x %s y3 = ffffffffffffffff
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 8000000000000000
 x | y = ffffffffffffffff
@@ -822,6 +1146,18 @@ x /u y2 = ffffffffffffffff
 x %u y2 = 0
 x /s y3 = ffffffffffffffff
 x %s y3 = 0
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 100000003
 x | y = ffffffffffffffff
@@ -852,6 +1188,18 @@ x /u y2 = 29b51243c
 x %u y2 = 2db954e7
 x /s y3 = 0
 x %s y3 = ffffffffffffffff
+x /u 3 = 5555555555555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffffffffffff
+x /u 5 = 3333333333333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffffffffffff
+x /u 11 = 1745d1745d1745d1
+x %u 11 = 4
+x /s 11 = 0
+x %s 11 = ffffffffffffffff
 ~x = 0
 x & y = 62354cda6226d1f3
 x | y = ffffffffffffffff
@@ -882,6 +1230,18 @@ x /u y2 = 8f947f37
 x %u y2 = 6065753d
 x /s y3 = 706b80c92f2f09fa
 x %s y3 = 0
+x /u 3 = 2fdc2a679af05202
+x %u 3 = 0
+x /s 3 = da86d512459afcad
+x %s 3 = ffffffffffffffff
+x /u 5 = 1cb74ca49029cace
+x %u 5 = 0
+x /s 5 = e98419715cf6979b
+x %s 5 = ffffffffffffffff
+x /u 11 = d0d7fedb5e47374
+x %u 11 = a
+x /s 11 = f5c7ae7958cd2da4
+x %s 11 = fffffffffffffffa
 ~x = 706b80c92f2f09f9
 x & y = 8f947f36d0d0f606
 x | y = ffffffffffffffff
@@ -912,6 +1272,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 0
 x | y = 7fffffff
@@ -942,6 +1314,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 1
 x | y = 7fffffff
@@ -972,6 +1356,18 @@ x /u y2 = 0
 x %u y2 = 7fffffff
 x /s y3 = ffffffff80000001
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 7fffffff
 x | y = ffffffffffffffff
@@ -1002,6 +1398,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 7fffffff
 x | y = 7fffffff
@@ -1032,6 +1440,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 0
 x | y = ffffffff
@@ -1062,6 +1482,18 @@ x /u y2 = 1
 x %u y2 = 0
 x /s y3 = 1
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 7fffffff
 x | y = 7fffffffffffffff
@@ -1092,6 +1524,18 @@ x /u y2 = 0
 x %u y2 = 7fffffff
 x /s y3 = 0
 x %s y3 = 7fffffff
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 0
 x | y = 800000007fffffff
@@ -1122,6 +1566,18 @@ x /u y2 = 7fffffff
 x %u y2 = 0
 x /s y3 = 7fffffff
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 3
 x | y = 17fffffff
@@ -1152,6 +1608,18 @@ x /u y2 = 6
 x %u y2 = 67c8b5f
 x /s y3 = 6
 x %s y3 = 67c8b5f
+x /u 3 = 2aaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaa
+x %s 3 = 1
+x /u 5 = 19999999
+x %u 5 = 2
+x /s 5 = 19999999
+x %s 5 = 2
+x /u 11 = ba2e8ba
+x %u 11 = 1
+x /s 11 = ba2e8ba
+x %s 11 = 1
 ~x = ffffffff80000000
 x & y = 4fadba5d
 x | y = 144093707fffffff
@@ -1182,6 +1650,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 1e607d2f69822238
+x %u 3 = 0
+x /s 3 = 1e607d2f69822238
+x %s 3 = 0
+x /u 5 = 1239e4b60c1ae154
+x %u 5 = 4
+x /s 5 = 1239e4b60c1ae154
+x %s 5 = 4
+x /u 11 = 848dc52bfaf209a
+x %u 11 = a
+x /s 11 = 848dc52bfaf209a
+x %s 11 = a
 ~x = a4de8871c3799957
 x & y = 3c8666a8
 x | y = 5b21778e7fffffff
@@ -1212,6 +1692,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 0
 x | y = 80000000
@@ -1242,6 +1734,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 0
 x | y = 80000001
@@ -1272,6 +1776,18 @@ x /u y2 = 0
 x %u y2 = 80000000
 x /s y3 = ffffffff80000000
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 80000000
 x | y = ffffffffffffffff
@@ -1302,6 +1818,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 0
 x | y = ffffffff
@@ -1332,6 +1860,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 80000000
 x | y = 80000000
@@ -1362,6 +1902,18 @@ x /u y2 = 1
 x %u y2 = 1
 x /s y3 = 1
 x %s y3 = 1
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 80000000
 x | y = 7fffffffffffffff
@@ -1392,6 +1944,18 @@ x /u y2 = 1
 x %u y2 = 0
 x /s y3 = ffffffffffffffff
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 0
 x | y = 8000000080000000
@@ -1422,6 +1986,18 @@ x /u y2 = 80000000
 x %u y2 = 0
 x /s y3 = 80000000
 x %s y3 = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 0
 x | y = 180000003
@@ -1452,6 +2028,18 @@ x /u y2 = 1
 x %u y2 = 467a43f
 x /s y3 = 1
 x %s y3 = 467a43f
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = 2aaaaaaa
+x %s 3 = 2
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = 19999999
+x %s 5 = 3
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = ba2e8ba
+x %s 11 = 2
 ~x = ffffffff7fffffff
 x & y = 80000000
 x | y = 7b985bc1e7bce4d7
@@ -1482,6 +2070,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 261ba3127a17215e
+x %u 3 = 0
+x /s 3 = 261ba3127a17215e
+x %s 3 = 0
+x /u 5 = 16dd61d7e2daad9e
+x %u 5 = 4
+x /s 5 = 16dd61d7e2daad9e
+x %s 5 = 4
+x /u 11 = a64a0d67e636630
+x %u 11 = a
+x /s 11 = a64a0d67e636630
+x %s 11 = a
 ~x = 8dad16c891ba9be5
 x & y = 0
 x | y = 7252e937ee45641a
@@ -1512,6 +2112,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 0
 x | y = 7fffffffffffffff
@@ -1542,6 +2154,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 1
 x | y = 7fffffffffffffff
@@ -1572,6 +2196,18 @@ x /u y2 = 80000000
 x %u y2 = 7fffffff
 x /s y3 = 8000000000000001
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 7fffffffffffffff
 x | y = ffffffffffffffff
@@ -1602,6 +2238,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 7fffffff
 x | y = 7fffffffffffffff
@@ -1632,6 +2280,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 80000000
 x | y = 7fffffffffffffff
@@ -1662,6 +2322,18 @@ x /u y2 = 100000002
 x %u y2 = 1
 x /s y3 = 100000002
 x %s y3 = 1
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 7fffffffffffffff
 x | y = 7fffffffffffffff
@@ -1692,6 +2364,18 @@ x /u y2 = ffffffff
 x %u y2 = 7fffffff
 x /s y3 = ffffffff00000001
 x %s y3 = 7fffffff
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 0
 x | y = ffffffffffffffff
@@ -1722,6 +2406,18 @@ x /u y2 = 7fffffffffffffff
 x %u y2 = 0
 x /s y3 = 7fffffffffffffff
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 100000003
 x | y = 7fffffffffffffff
@@ -1752,6 +2448,18 @@ x /u y2 = ca1d702e
 x %u y2 = 372ea79b
 x /s y3 = fffffffea2f0285c
 x %s y3 = 46eadf37
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 1
+x /s 3 = 2aaaaaaaaaaaaaaa
+x %s 3 = 1
+x /u 5 = 1999999999999999
+x %u 5 = 2
+x /s 5 = 1999999999999999
+x %s 5 = 2
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 7
+x /s 11 = ba2e8ba2e8ba2e8
+x %s 11 = 7
 ~x = 8000000000000000
 x & y = 2220229ec164ffe1
 x | y = ffffffffffffffff
@@ -1782,6 +2490,18 @@ x /u y2 = bafa9b4b
 x %u y2 = 608b627
 x /s y3 = bafa9b4b
 x %s y3 = 608b627
+x /u 3 = 1f29c48c43af5e49
+x %u 3 = 1
+x /s 3 = 1f29c48c43af5e49
+x %s 3 = 1
+x /u 5 = 12b2a920f5693892
+x %u 5 = 2
+x /s 5 = 12b2a920f5693892
+x %s 5 = 2
+x /u 11 = 87fc13d86d2bc9f
+x %u 11 = 7
+x /s 11 = 87fc13d86d2bc9f
+x %s 11 = 7
 ~x = a282b25b34f1e523
 x & y = 5d7d4da4cb0e1adc
 x | y = 7fffffffffffffff
@@ -1812,6 +2532,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 0
 x | y = 8000000000000000
@@ -1842,6 +2574,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 0
 x | y = 8000000000000001
@@ -1872,6 +2616,18 @@ x /u y2 = 80000000
 x %u y2 = 80000000
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 8000000000000000
 x | y = ffffffffffffffff
@@ -1902,6 +2658,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 0
 x | y = 800000007fffffff
@@ -1932,6 +2700,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 0
 x | y = 8000000080000000
@@ -1962,6 +2742,18 @@ x /u y2 = 100000002
 x %u y2 = 2
 x /s y3 = fffffffefffffffe
 x %s y3 = fffffffffffffffe
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 0
 x | y = ffffffffffffffff
@@ -1992,6 +2784,18 @@ x /u y2 = 100000000
 x %u y2 = 0
 x /s y3 = 100000000
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 8000000000000000
 x | y = 8000000000000000
@@ -2022,6 +2826,18 @@ x /u y2 = 8000000000000000
 x %u y2 = 0
 x /s y3 = 8000000000000000
 x %s y3 = 0
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 0
 x | y = 8000000100000003
@@ -2052,6 +2868,18 @@ x /u y2 = a4795a4ab
 x %u y2 = 13c1551
 x /s y3 = fffffff5b86a5b55
 x %s y3 = fffffffffec3eaaf
+x /u 3 = 2aaaaaaaaaaaaaaa
+x %u 3 = 2
+x /s 3 = d555555555555556
+x %s 3 = fffffffffffffffe
+x /u 5 = 1999999999999999
+x %u 5 = 3
+x /s 5 = e666666666666667
+x %s 5 = fffffffffffffffd
+x /u 11 = ba2e8ba2e8ba2e8
+x %u 11 = 8
+x /s 11 = f45d1745d1745d18
+x %s 11 = fffffffffffffff8
 ~x = 7fffffffffffffff
 x & y = 0
 x | y = 8c73aa0d9a415dfb
@@ -2082,6 +2910,18 @@ x /u y2 = 31d220f5
 x %u y2 = 399b8b6e
 x /s y3 = ffffffffce2ddf0b
 x %s y3 = 399b8b6e
+x /u 3 = 84db028e8892e7a
+x %u 3 = 0
+x /s 3 = 84db028e8892e7a
+x %s 3 = 0
+x /u 5 = 4fb69b2251f1be2
+x %u 5 = 4
+x /s 5 = 4fb69b2251f1be2
+x %s 5 = 4
+x /u 11 = 243bbae10df984f
+x %u 11 = 9
+x /s 11 = 243bbae10df984f
+x %s 11 = 9
 ~x = e716ef8546647491
 x & y = 0
 x | y = 98e9107ab99b8b6e
@@ -2112,6 +2952,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 0
 x | y = 100000003
@@ -2142,6 +2994,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 1
 x | y = 100000003
@@ -2172,6 +3036,18 @@ x /u y2 = 1
 x %u y2 = 4
 x /s y3 = fffffffefffffffd
 x %s y3 = 0
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 100000003
 x | y = ffffffffffffffff
@@ -2202,6 +3078,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 3
 x | y = 17fffffff
@@ -2232,6 +3120,18 @@ x /u y2 = 0
 x %u y2 = 0
 x /s y3 = 0
 x %s y3 = 0
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 0
 x | y = 180000003
@@ -2262,6 +3162,18 @@ x /u y2 = 2
 x %u y2 = 5
 x /s y3 = 2
 x %s y3 = 5
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 100000003
 x | y = 7fffffffffffffff
@@ -2292,6 +3204,18 @@ x /u y2 = 2
 x %u y2 = 3
 x /s y3 = fffffffffffffffe
 x %s y3 = 3
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 0
 x | y = 8000000100000003
@@ -2322,6 +3246,18 @@ x /u y2 = 100000003
 x %u y2 = 0
 x /s y3 = 100000003
 x %s y3 = 0
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 100000003
 x | y = 100000003
@@ -2352,6 +3288,18 @@ x /u y2 = 1
 x %u y2 = 16432d9b
 x /s y3 = fffffffffffffff5
 x %s y3 = b1d0a7b
+x /u 3 = 55555556
+x %u 3 = 1
+x /s 3 = 55555556
+x %s 3 = 1
+x /u 5 = 33333333
+x %u 5 = 4
+x /s 5 = 33333333
+x %s 5 = 4
+x /u 11 = 1745d174
+x %u 11 = 7
+x /s 11 = 1745d174
+x %s 11 = 7
 ~x = fffffffefffffffc
 x & y = 1
 x | y = e9bcd26990f095a7
@@ -2382,6 +3330,18 @@ x /u y2 = 329cb23ce0f7aa50
 x %u y2 = 0
 x /s y3 = 329cb23ce0f7aa50
 x %s y3 = 0
+x /u 3 = 10dee6144afd38c5
+x %u 3 = 1
+x /s 3 = 10dee6144afd38c5
+x %s 3 = 1
+x /u 5 = a1f56d8f9cb2210
+x %u 5 = 0
+x /s 5 = a1f56d8f9cb2210
+x %s 5 = 0
+x /u 11 = 499e1a8718ae0f0
+x %u 11 = 0
+x /s 11 = 499e1a8718ae0f0
+x %s 11 = 0
 ~x = cd634dc31f0855af
 x & y = 0
 x | y = 329cb23de0f7aa53
@@ -2412,6 +3372,18 @@ x /u y2 = 86cb918b
 x %u y2 = 910b6dd3
 x /s y3 = 133e437097
 x %s y3 = fffffffffe99a023
+x /u 3 = 2bcb8e3115aa0b1f
+x %u 3 = 2
+x /s 3 = d67638dbc054b5cb
+x %s 3 = fffffffffffffffe
+x /u 5 = 1a46eeea4032d379
+x %u 5 = 2
+x /s 5 = e713bbb70cffa047
+x %s 5 = fffffffffffffffc
+x /u 11 = bf1b26a7a45a5f1
+x %u 11 = 4
+x /s 11 = f4abe0f61d2e6020
+x %s 11 = ffffffffffffffff
 ~x = 7c9d556cbf01dea0
 x & y = 8102200000ec0002
 x | y = fbe6beb756fea15f
@@ -2442,6 +3414,18 @@ x /u y2 = 84c9e8f3
 x %u y2 = 27966e44
 x /s y3 = 84c9e8f3
 x %s y3 = 27966e44
+x /u 3 = 122ad667ce8c5538
+x %u 3 = 1
+x /s 3 = 122ad667ce8c5538
+x %s 3 = 1
+x /u 5 = ae680a4af20ffee
+x %u 5 = 3
+x /s 5 = ae680a4af20ffee
+x %s 5 = 3
+x /u 11 = 4f4690509c92e83
+x %u 11 = 8
+x /s 11 = 4f4690509c92e83
+x %s 11 = 8
 ~x = c97f7cc8945b0056
 x & y = 2000820723804900
 x | y = 7f92b377ffbeffad
@@ -2472,6 +3456,18 @@ x /u y2 = e9932394
 x %u y2 = bed9fbb
 x /s y3 = 142f786e7
 x %s y3 = ffffffffe6446d5d
+x /u 3 = 3a53921f27b11bab
+x %u 3 = 2
+x /s 3 = e4fe3cc9d25bc657
+x %s 3 = fffffffffffffffe
+x /u 5 = 22fef145e49d7700
+x %u 5 = 3
+x /s 5 = efcbbe12b16a43ce
+x %s 5 = fffffffffffffffd
+x /u 11 = fe83f1fc501c1ba
+x %u 11 = 5
+x /s 11 = f8a26dab67ea7be9
+x %s 11 = 0
 ~x = 510549a288ecacfc
 x & y = aec2264830121102
 x | y = bffff67ff7bbd7d7
@@ -2502,6 +3498,18 @@ x /u y2 = 49889cbcc
 x %u y2 = d961931
 x /s y3 = ffffffff5078c8f7
 x %s y3 = fffffffffb32ee6a
+x /u 3 = 4a4153351cb255f9
+x %u 3 = 2
+x /s 3 = f4ebfddfc75d00a5
+x %s 3 = fffffffffffffffe
+x /u 5 = 2c8d98531137cd2f
+x %u 5 = 2
+x /s 5 = f95a651fde0499fd
+x %s 5 = fffffffffffffffc
+x /u 11 = 14405c82d947e8e7
+x %u 11 = 0
+x /s 11 = fcfa8b0e7c30a316
+x %s 11 = fffffffffffffffb
 ~x = 213c0660a9e8fe12
 x & y = 10409095561000e8
 x | y = fefbfbdffe5f6bfd
@@ -2532,6 +3540,18 @@ x /u y2 = 111c647a7
 x %u y2 = 2a35fbed
 x /s y3 = 111c647a7
 x %s y3 = 2a35fbed
+x /u 3 = 295ca3b37973c7a2
+x %u 3 = 1
+x /s 3 = 295ca3b37973c7a2
+x %s 3 = 1
+x /u 5 = 18d12f0548df1161
+x %u 5 = 2
+x /s 5 = 18d12f0548df1161
+x %s 5 = 2
+x /u 11 = b47cf8e09d9c215
+x %u 11 = 0
+x /s 11 = b47cf8e09d9c215
+x %s 11 = 0
 ~x = 83ea14e593a4a918
 x & y = 740588126c0140e2
 x | y = 7c17ef7e7c5f76ef
@@ -2562,6 +3582,18 @@ x /u y2 = 67e883b7
 x %u y2 = 4d949d8f
 x /s y3 = 67e883b7
 x %s y3 = 4d949d8f
+x /u 3 = f0e444b6fdfe025
+x %u 3 = 2
+x /s 3 = f0e444b6fdfe025
+x %s 3 = 2
+x /u 5 = 9088f6076532016
+x %u 5 = 3
+x /s 5 = 9088f6076532016
+x %s 5 = 3
+x /u 11 = 41b29e6073d0e95
+x %u 11 = a
+x /s 11 = 41b29e6073d0e95
+x %s 11 = a
 ~x = d2d5331db0605f8e
 x & y = 2d02482204938020
 x | y = 6f6fecee5fdfe47d
@@ -2592,6 +3624,18 @@ x /u y2 = 203527d3
 x %u y2 = 339f3657
 x /s y3 = ffffffffcf52411e
 x %s y3 = 47c75183
+x /u 3 = 67605b7f984f059
+x %u 3 = 0
+x /s 3 = 67605b7f984f059
+x %s 3 = 0
+x /u 5 = 3e069d4c8e95d02
+x %u 5 = 1
+x /s 5 = 3e069d4c8e95d02
+x %s 5 = 1
+x /u 11 = 1c318d5158158d2
+x %u 11 = 5
+x /s 11 = 1c318d5158158d2
+x %s 11 = 5
 ~x = ec9deed813712ef4
 x & y = 12001124448c910a
 x | y = 9b729dfffd9ff53f
@@ -2622,6 +3666,18 @@ x /u y2 = 57ad3b593
 x %u y2 = 7501355
 x /s y3 = 57ad3b593
 x %s y3 = 7501355
+x /u 3 = 18e5589b620ab511
+x %u 3 = 2
+x /s 3 = 18e5589b620ab511
+x %s 3 = 2
+x /u 5 = ef001f6d46cd30a
+x %u 5 = 3
+x /s 5 = ef001f6d46cd30a
+x %s 5 = 3
+x /u 11 = 6ca2f703202eb90
+x %u 11 = 5
+x /s 11 = 6ca2f703202eb90
+x %s 11 = 5
 ~x = b54ff62dd9dfe0ca
 x & y = 8a0008000200820
 x | y = 4fb139f2a6615fb5
@@ -2652,6 +3708,18 @@ x /u y2 = 3affbc857
 x %u y2 = 2cd84c77
 x /s y3 = fffffffe19aa1e7c
 x %s y3 = ffffffffe134208f
+x /u 3 = 385181e6dae2e1cf
+x %u 3 = 2
+x /s 3 = e2fc2c91858d8c7b
+x %s 3 = fffffffffffffffe
+x /u 5 = 21ca81241cee877c
+x %u 5 = 3
+x /s 5 = ee974df0e9bb544a
+x %s 5 = fffffffffffffffd
+x /u 11 = f5c0c27b00f54db
+x %u 11 = 6
+x /s 11 = f8163ab352f80f0b
+x %s 11 = fffffffffffffff6
 ~x = 570b7a4b6f575a90
 x & y = 28d0818000a8a442
 x | y = adf5b7fcdcb9a7ff
@@ -2682,6 +3750,18 @@ x /u y2 = ed62a033
 x %u y2 = 9a9c1784
 x /s y3 = 1317fc5dc
 x %s y3 = ffffffffdaba2cf5
+x /u 3 = 3980e6c0ff575613
+x %u 3 = 0
+x /s 3 = e42b916baa0200be
+x %s 3 = ffffffffffffffff
+x /u 5 = 22808a73cc679a0b
+x %u 5 = 2
+x /s 5 = ef4d5740993466d9
+x %s 5 = fffffffffffffffc
+x /u 11 = faeca91ba008bd6
+x %u 11 = 7
+x /s 11 = f868f91d5ce94606
+x %s 11 = fffffffffffffff7
 ~x = 537d4bbd01f9fdc6
 x & y = a8008042d0040010
 x | y = be8bf577febf2e7d
@@ -2712,6 +3792,18 @@ x /u y2 = 1457fa721
 x %u y2 = 62f7b025
 x /s y3 = aca563d9
 x %s y3 = fffffffffc51c715
+x /u 3 = 3b2ad00c14d8a806
+x %u 3 = 1
+x /s 3 = e5d57ab6bf8352b1
+x %s 3 = 0
+x /u 5 = 2380166da61b9803
+x %u 5 = 4
+x /s 5 = f04ce33a72e864d1
+x %s 5 = fffffffffffffffe
+x /u 11 = 1022f2ec05af73a4
+x %u 11 = 7
+x /s 11 = f8dd2177a8982dd4
+x %s 11 = fffffffffffffff7
 ~x = 4e7f8fdbc17607ec
 x & y = 818040242e888802
 x | y = bb9a702e7ec9f9b7
@@ -2742,6 +3834,18 @@ x /u y2 = 401f99d2e
 x %u y2 = 1b8b48d5
 x /s y3 = fffffffc1b6b5e46
 x %s y3 = ffffffffebae19b5
+x /u 3 = 2b4968cb1b85047f
+x %u 3 = 0
+x /s 3 = d5f41375c62faf2a
+x %s 3 = ffffffffffffffff
+x /u 5 = 19f8d879dd4fcf7f
+x %u 5 = 2
+x /s 5 = e6c5a546aa1c9c4d
+x %s 5 = fffffffffffffffc
+x /u 11 = bce33da4d52d2ae
+x %u 11 = 3
+x /s 11 = f4886265f03b8cdd
+x %s 11 = fffffffffffffffe
 ~x = 7e23c59ead70f282
 x & y = 440a40428e0148
 x | y = a1ff3eed77ffef7d
@@ -2772,6 +3876,18 @@ x /u y2 = 1cdd42781
 x %u y2 = 8307e40
 x /s y3 = 1cdd42781
 x %s y3 = 8307e40
+x /u 3 = 6d86bd5739f6452
+x %u 3 = 1
+x /s 3 = 6d86bd5739f6452
+x %s 3 = 1
+x /u 5 = 41b73e67892d5cb
+x %u 5 = 0
+x /s 5 = 41b73e67892d5cb
+x %s 5 = 0
+x /u 11 = 1ddeedd1f888fb9
+x %u 11 = 4
+x /s 11 = 1ddeedd1f888fb9
+x %s 11 = 4
 ~x = eb76bc7fa521d308
 x & y = 200088620b2
 x | y = 1feb73b7fadefdff
@@ -2802,6 +3918,18 @@ x /u y2 = 1ac3a0a48
 x %u y2 = f8ff129
 x /s y3 = 1ac3a0a48
 x %s y3 = f8ff129
+x /u 3 = 11dcf2a0d0c46c55
+x %u 3 = 2
+x /s 3 = 11dcf2a0d0c46c55
+x %s 3 = 2
+x /u 5 = ab7c4c6e3a90dcd
+x %u 5 = 0
+x /s 5 = ab7c4c6e3a90dcd
+x %s 5 = 0
+x /u 11 = 4df2ae60a641d8b
+x %u 11 = 8
+x /s 11 = 4df2ae60a641d8b
+x %s 11 = 8
 ~x = ca69281d8db2bafe
 x & y = 200051a2504d0100
 x | y = 359fd7e3fbcd657d
@@ -2832,6 +3960,18 @@ x /u y2 = 2464000e3
 x %u y2 = d195088
 x /s y3 = fffffffdd7d46212
 x %s y3 = fffffffffcbb11e9
+x /u 3 = 2bcc4928c5bfa2b3
+x %u 3 = 2
+x /s 3 = d676f3d3706a4d5f
+x %s 3 = fffffffffffffffe
+x /u 5 = 1a475f1876a62e6b
+x %u 5 = 4
+x /s 5 = e7142be54372fb39
+x %s 5 = fffffffffffffffe
+x /u 11 = bf1e56835ee7231
+x %u 11 = 0
+x /s 11 = f4ac13f3d8d72c60
+x %s 11 = fffffffffffffffb
 ~x = 7c9b2485aec117e4
 x & y = 14419101012a00a
 x | y = bbe5fffbd17efb1f
@@ -2862,6 +4002,18 @@ x /u y2 = 195403f42
 x %u y2 = 67e00199
 x /s y3 = ffffffff94c3b859
 x %s y3 = ffffffffd787355f
+x /u 3 = 437a4bcf93f8f997
+x %u 3 = 0
+x /s 3 = ee24f67a3ea3a442
+x %s 3 = ffffffffffffffff
+x /u 5 = 287c93e2f2622f5a
+x %u 5 = 3
+x /s 5 = f54960afbf2efc28
+x %s 5 = fffffffffffffffd
+x /u 11 = 12672bf2cb43e6fa
+x %u 11 = 7
+x /s 11 = fb215a7e6e2ca12a
+x %s 11 = fffffffffffffff7
 ~x = 35911c914415133a
 x & y = 4a60e14691c0c8c0
 x | y = ffeee7fefffbfef5
@@ -2892,6 +4044,18 @@ x /u y2 = 292cea58
 x %u y2 = 301cdf07
 x /s y3 = 292cea58
 x %s y3 = 301cdf07
+x /u 3 = 4dd7b8dc788047f
+x %u 3 = 2
+x /s 3 = 4dd7b8dc788047f
+x %s 3 = 2
+x /u 5 = 2eb4a21de1e6919
+x %u 5 = 2
+x /s 5 = 2eb4a21de1e6919
+x %s 5 = 2
+x /u 11 = 153ad55366ae9f4
+x %u 11 = 3
+x /s 11 = 153ad55366ae9f4
+x %s 11 = 3
 ~x = f1678d56a967f280
 x & y = a98120904980122
 x | y = 5ebefbad7fbeedff
@@ -2922,6 +4086,18 @@ x /u y2 = ce682040
 x %u y2 = 8882909
 x /s y3 = 16845c4311
 x %s y3 = fffffffffe31f1da
+x /u 3 = 4430365b0a64d843
+x %u 3 = 0
+x /s 3 = eedae105b50f82ee
+x %s 3 = ffffffffffffffff
+x /u 5 = 28e9ba369fd61b5b
+x %u 5 = 2
+x /s 5 = f5b687036ca2e829
+x %s 5 = fffffffffffffffc
+x /u 11 = 1298c9018e789812
+x %u 11 = 3
+x /s 11 = fb52f78d31615241
+x %s 11 = fffffffffffffffe
 ~x = 336f5ceee0d17736
 x & y = cc902111112e0080
 x | y = fdb7bbffdf6ecbed
@@ -2952,6 +4128,18 @@ x /u y2 = ff48210c
 x %u y2 = 6c4e224b
 x /s y3 = 114ef78ac
 x %s y3 = ffffffffff84590b
+x /u 3 = 524579262dee95b6
+x %u 3 = 1
+x /s 3 = fcf023d0d8994061
+x %s 3 = 0
+x /u 5 = 315ce24a1b8f26a0
+x %u 5 = 3
+x /s 5 = fe29af16e85bf36e
+x %s 5 = fffffffffffffffd
+x /u 11 = 167009c49829cbbd
+x %u 11 = 4
+x /s 11 = ff2a38503b1285ec
+x %s 11 = ffffffffffffffff
 ~x = 92f948d76343edc
 x & y = f68021120043c122
 x | y = f7d27b729befd177
@@ -2982,6 +4170,18 @@ x /u y2 = 27bb1964
 x %u y2 = 7672b2b1
 x /s y3 = ffffffff68dce4e4
 x %s y3 = 1d207631
+x /u 3 = a7ca1b7e214f459
+x %u 3 = 2
+x /s 3 = a7ca1b7e214f459
+x %s 3 = 2
+x /u 5 = 64ac76e5472f902
+x %u 5 = 3
+x /s 5 = 64ac76e5472f902
+x %s 5 = 3
+x /u 11 = 2dc2c1ae09159e9
+x %u 11 = a
+x /s 11 = 2dc2c1ae09159e9
+x %s 11 = a
 ~x = e08a1ad859c122f2
 x & y = a340027a42ecd08
 x | y = dff7ff6fe6bedf9d
@@ -3012,6 +4212,18 @@ x /u y2 = 28349b7ce
 x %u y2 = 24b397b7
 x /s y3 = 28349b7ce
 x %s y3 = 24b397b7
+x /u 3 = 229daae6f2322257
+x %u 3 = 2
+x /s 3 = 229daae6f2322257
+x %s 3 = 2
+x /u 5 = 14c500242aeae167
+x %u 5 = 4
+x /s 5 = 14c500242aeae167
+x %s 5 = 4
+x /u 11 = 970d184cdb09500
+x %u 11 = 7
+x /s 11 = 970d184cdb09500
+x %s 11 = 7
 ~x = 9826ff4b296998f8
 x & y = 2151001050060602
 x | y = 6fdba6bcde97778f
@@ -3042,6 +4254,18 @@ x /u y2 = 12c706881
 x %u y2 = 3974fe7b
 x /s y3 = fffffffefe5ea0d2
 x %s y3 = ffffffffe980f385
+x /u 3 = 2df08781ae624f30
+x %u 3 = 1
+x /s 3 = d89b322c590cf9db
+x %s 3 = 0
+x /u 5 = 1b90514dcf07c91d
+x %u 5 = 0
+x /s 5 = e85d1e1a9bd495ea
+x %s 5 = ffffffffffffffff
+x /u 11 = c876ac646d4fe53
+x %u 11 = 0
+x /s 11 = f5419951e9bdb882
+x %s 11 = fffffffffffffffb
 ~x = 762e697af4d9126e
 x & y = 14094040a262080
 x | y = fdfff6978f7fffdd
@@ -3072,6 +4296,18 @@ x /u y2 = 2e1d4dc
 x %u y2 = cb2df2bf
 x /s y3 = fffffffff2ac0c93
 x %s y3 = 2a546e24
+x /u 3 = ca370abf90e10e
+x %u 3 = 1
+x /s 3 = ca370abf90e10e
+x %s 3 = 1
+x /u 5 = 795439a623ba3b
+x %u 5 = 4
+x /s 5 = 795439a623ba3b
+x %s 5 = 4
+x /u 11 = 372648bfe1b1be
+x %u 11 = 1
+x /s 11 = 372648bfe1b1be
+x %s 11 = 1
 ~x = fda15adfc14d5cd4
 x & y = 25aa0201682800a
 x | y = d27fb73d7ff7a7ff
@@ -3102,6 +4338,18 @@ x /u y2 = 98de5aed
 x %u y2 = 81b9d719
 x /s y3 = ffffffff312686c0
 x %s y3 = 67db7555
+x /u 3 = 1d4d2c23df3354c7
+x %u 3 = 0
+x /s 3 = 1d4d2c23df3354c7
+x %s 3 = 0
+x /u 5 = 1194b41585eb9944
+x %u 5 = 1
+x /s 5 = 1194b41585eb9944
+x %s 5 = 1
+x /u 11 = 7fdc638542545aa
+x %u 11 = 7
+x /s 11 = 7fdc638542545aa
+x %s 11 = 7
 ~x = a8187b94626601aa
 x & y = 1325002814186040
 x | y = d7f7d4efdd9fff55
@@ -3132,6 +4380,18 @@ x /u y2 = 2637b00b
 x %u y2 = 4a30bdb
 x /s y3 = 2637b00b
 x %s y3 = 4a30bdb
+x /u 3 = 2a81370cf14732f
+x %u 3 = 2
+x /s 3 = 2a81370cf14732f
+x %s 3 = 2
+x /u 5 = 1980baa15d911e9
+x %u 5 = 2
+x /s 5 = 1980baa15d911e9
+x %s 5 = 2
+x /u 11 = b979aa670593c7
+x %u 11 = 2
+x /s 11 = b979aa670593c7
+x %s 11 = 2
 ~x = f807c5ad92c2a670
 x & y = 56030102c191002
 x | y = 37fa7fde6ffd79ff
@@ -3162,6 +4422,18 @@ x /u y2 = 2149e9078
 x %u y2 = 3157ec11
 x /s y3 = ffffffffbbb6b39e
 x %s y3 = ffffffff9f7efd07
+x /u 3 = 4ba2da01fefd311d
+x %u 3 = 2
+x /s 3 = f64d84aca9a7dbc9
+x %s 3 = fffffffffffffffe
+x /u 5 = 2d61b6013297ea45
+x %u 5 = 0
+x /s 5 = fa2e82cdff64b712
+x %s 5 = ffffffffffffffff
+x /u 11 = 14a0c717d12dc793
+x %u 11 = 8
+x /s 11 = fd5af5a3741681c3
+x %s 11 = fffffffffffffff8
 ~x = 1d1771fa03086ca6
 x & y = 600880056cd28250
 x | y = efefef87fff79ffd
@@ -3192,6 +4464,18 @@ x /u y2 = 178126fd
 x %u y2 = 75bd3a7
 x /s y3 = ffffffffe1f1945e
 x %s y3 = 5ca580ab
+x /u 3 = 465888d92c88f66
+x %u 3 = 1
+x /s 3 = 465888d92c88f66
+x %s 3 = 1
+x /u 5 = 2a351ee8b4522d7
+x %u 5 = 0
+x /s 5 = 2a351ee8b4522d7
+x %s 5 = 0
+x /u 11 = 132f6b23f4df890
+x %u 11 = 3
+x /s 11 = 132f6b23f4df890
+x %s 11 = 3
 ~x = f2cf665747a651cc
 x & y = d20182820412c02
 x | y = 8fb8d9fcfc5def77
@@ -3222,6 +4506,18 @@ x /u y2 = 3aa02d06b
 x %u y2 = 8d30eae
 x /s y3 = fffffffe83ee35ed
 x %s y3 = ffffffffdeff9c14
+x /u 3 = 3cba371623852589
+x %u 3 = 2
+x /s 3 = e764e1c0ce2fd035
+x %s 3 = fffffffffffffffe
+x /u 5 = 246fbaa6e21cb01f
+x %u 5 = 2
+x /s 5 = f13c8773aee97ced
+x %s 5 = fffffffffffffffc
+x /u 11 = 108fe07a66c738c8
+x %u 11 = 5
+x /s 11 = f94a0f0609aff2f7
+x %s 11 = 0
 ~x = 49d15abd95708f62
 x & y = 30288500028d2088
 x | y = b7bea5cf6adf7ffd
@@ -3252,6 +4548,18 @@ x /u y2 = 7cd84df1
 x %u y2 = 1c098191
 x /s y3 = 7cd84df1
 x %s y3 = 1c098191
+x /u 3 = f86ee25fc5c5707
+x %u 3 = 2
+x /s 3 = f86ee25fc5c5707
+x %s 3 = 2
+x /u 5 = 950f549fdd10104
+x %u 5 = 3
+x /s 5 = 950f549fdd10104
+x %s 5 = 3
+x /u 11 = 43c1267735f0076
+x %u 11 = 5
+x /s 11 = 43c1267735f0076
+x %s 11 = 5
 ~x = d16b358e0aeafae8
 x & y = e84486044000512
 x | y = 7f94cff7f517cf5f
@@ -3282,6 +4590,18 @@ x /u y2 = 511ed4ac8
 x %u y2 = 27f86a1
 x /s y3 = 511ed4ac8
 x %s y3 = 27f86a1
+x /u 3 = 20945a3de80c88b5
+x %u 3 = 2
+x /s 3 = 20945a3de80c88b5
+x %s 3 = 2
+x /u 5 = 138c362524d45206
+x %u 5 = 3
+x /s 5 = 138c362524d45206
+x %s 5 = 3
+x /u 11 = 8e2a43f6dd4df77
+x %u 11 = 4
+x /s 11 = 8e2a43f6dd4df77
+x %s 11 = 4
 ~x = 9e42f14647da65de
 x & y = 10506b038249800
 x | y = 73ff1ff9feaffa3d
@@ -3312,6 +4632,18 @@ x /u y2 = 751173e7
 x %u y2 = 4f1d5ff0
 x /s y3 = ffffffff88c0657c
 x %s y3 = 3027aaf
+x /u 3 = 13b0fe02eb2e5613
+x %u 3 = 2
+x /s 3 = 13b0fe02eb2e5613
+x %s 3 = 2
+x /u 5 = bd0986826b566d8
+x %u 5 = 3
+x /s 5 = bd0986826b566d8
+x %s 5 = 3
+x /u 11 = 55ed0e985f55d4b
+x %u 11 = 2
+x /s 11 = 55ed0e985f55d4b
+x %s 11 = 2
 ~x = c4ed05f73e74fdc4
 x & y = 1025008c109022a
 x | y = bb3efbfdc3cb2abf
@@ -3342,6 +4674,18 @@ x /u y2 = a405e4b4
 x %u y2 = 4f86312d
 x /s y3 = a405e4b4
 x %s y3 = 4f86312d
+x /u 3 = 115e81465ce7714c
+x %u 3 = 1
+x /s 3 = 115e81465ce7714c
+x %s 3 = 1
+x /u 5 = a6be72a37be10c7
+x %u 5 = 2
+x /s 5 = a6be72a37be10c7
+x %s 5 = 2
+x /u 11 = 4bcaee4a4f94d71
+x %u 11 = a
+x /s 11 = 4bcaee4a4f94d71
+x %s 11 = a
 ~x = cbe47c2ce949ac1a
 x & y = 1013800210125380
 x | y = 755bbff73fffdbf5
@@ -3372,6 +4716,18 @@ x /u y2 = 7c9e1383
 x %u y2 = 89a32be1
 x /s y3 = fffffffe57830a86
 x %s y3 = 83cdb23
+x /u 3 = 201cac35b86dd88a
+x %u 3 = 1
+x /s 3 = 201cac35b86dd88a
+x %s 3 = 1
+x /u 5 = 134467536ea84eb9
+x %u 5 = 2
+x /s 5 = 134467536ea84eb9
+x %s 5 = 2
+x /u 11 = 8c2006bbdef699a
+x %u 11 = 1
+x /s 11 = 8c2006bbdef699a
+x %s 11 = 1
 ~x = 9fa9fb5ed6b67660
 x & y = 404600a000018102
 x | y = e5f6dceb2b6d9bdf
@@ -3402,6 +4758,18 @@ x /u y2 = 156e6b4cb
 x %u y2 = caae302
 x /s y3 = ffffffff09523710
 x %s y3 = ffffffffa5f4f199
+x /u 3 = 31a14ca0c328b5f8
+x %u 3 = 1
+x /s 3 = dc4bf74b6dd360a3
+x %s 3 = 0
+x /u 5 = 1dc72dfa0eb206c8
+x %u 5 = 1
+x /s 5 = ea93fac6db7ed395
+x %s 5 = 0
+x /u 11 = d8914e606ae0315
+x %u 11 = 2
+x /s 11 = f6434371a996bd44
+x %s 11 = fffffffffffffffd
 ~x = 6b1c1a1db685de16
 x & y = 42024c0414a0040
 x | y = ffebf7f7697f2fed
@@ -3432,6 +4800,18 @@ x /u y2 = 7fac2866
 x %u y2 = 15d50693
 x /s y3 = 7fac2866
 x %s y3 = 15d50693
+x /u 3 = ecb77d397fc3fc1
+x %u 3 = 0
+x /s 3 = ecb77d397fc3fc1
+x %s 3 = 0
+x /u 5 = 8e07b188e642640
+x %u 5 = 3
+x /s 5 = 8e07b188e642640
+x %s 5 = 3
+x /u 11 = 408f2226f44cb91
+x %u 11 = 8
+x /s 11 = 408f2226f44cb91
+x %s 11 = 8
 ~x = d39d9885380b40bc
 x & y = 862024886441d02
 x | y = 7cff7f7afffeff57
@@ -3462,6 +4842,18 @@ x /u y2 = 5d8f7413
 x %u y2 = 2f76d45d
 x /s y3 = fffffffcb6a49899
 x %s y3 = d7812bd
+x /u 3 = 1c10d99a006342b9
+x %u 3 = 2
+x /s 3 = 1c10d99a006342b9
+x %s 3 = 2
+x /u 5 = 10d6e8f6003b8e6f
+x %u 5 = 2
+x /s 5 = 10d6e8f6003b8e6f
+x %s 5 = 2
+x /u 11 = 7a7812a001b1232
+x %u 11 = 7
+x /s 11 = 7a7812a001b1232
+x %s 11 = 7
 ~x = abcd7331fed637d2
 x & y = 442084c000290028
 x | y = f6739efec53fcc3d
@@ -3492,6 +4884,18 @@ x /u y2 = 82583705
 x %u y2 = 41aecdc5
 x /s y3 = fffffffb038fcf10
 x %s y3 = 5628987
+x /u 3 = 276c2afb9a0e57b7
+x %u 3 = 2
+x /s 3 = 276c2afb9a0e57b7
+x %s 3 = 2
+x /u 5 = 17a74cfd5c6f016e
+x %u 5 = 1
+x /s 5 = 17a74cfd5c6f016e
+x %s 5 = 1
+x /u 11 = ac068d04149bad5
+x %u 11 = 0
+x /s 11 = ac068d04149bad5
+x %s 11 = 0
 ~x = 89bb7f0d31d4f8d8
 x & y = 604480724a230422
 x | y = fe47cdfacf3f1f2f
@@ -3522,6 +4926,18 @@ x /u y2 = 43622075f
 x %u y2 = 748637e
 x /s y3 = fffffffc38469f85
 x %s y3 = ffffffffeb6799d0
+x /u 3 = 2cf82160212b6e3b
+x %u 3 = 0
+x /s 3 = d7a2cc0acbd618e6
+x %s 3 = ffffffffffffffff
+x /u 5 = 1afb4739ad807556
+x %u 5 = 3
+x /s 5 = e7c814067a4d4224
+x %s 5 = fffffffffffffffd
+x /u 11 = c43ac02f1c606ca
+x %u 11 = 3
+x /s 11 = f4fdda8e94aec0f9
+x %s 11 = fffffffffffffffe
 ~x = 79179bdf9c7db54e
 x & y = 8042001004020
 x | y = a6e8f4ad7fe37bfd
@@ -3552,6 +4968,18 @@ x /u y2 = 4d288aa25
 x %u y2 = 9a2cc6c
 x /s y3 = ffffffffb9841949
 x %s y3 = ffffffffd933c240
+x /u 3 = 50b9779fd98dac6e
+x %u 3 = 1
+x /s 3 = fb64224a84385719
+x %s 3 = 0
+x /u 5 = 306f47c64f55010f
+x %u 5 = 0
+x /s 5 = fd3c14931c21cddc
+x %s 5 = ffffffffffffffff
+x /u 11 = 1604095a240f5d92
+x %u 11 = 5
+x /s 11 = febe37e5c6f817c1
+x %s 11 = 0
 ~x = dd399207356fab4
 x & y = 322464938020044a
 x | y = f23fefffefeda57f
@@ -3582,6 +5010,18 @@ x /u y2 = aebe580f
 x %u y2 = 47a4b5a3
 x /s y3 = aea5798d9
 x %s y3 = fffffffffe0cd097
+x /u 3 = 3870ea2956584f27
+x %u 3 = 0
+x /s 3 = e31b94d40102f9d2
+x %s 3 = ffffffffffffffff
+x /u 5 = 21dd594c009b62b1
+x %u 5 = 0
+x /s 5 = eeaa2618cd682f7e
+x %s 5 = ffffffffffffffff
+x /u 11 = f649cf40046a139
+x %u 11 = 2
+x /s 11 = f81ecb7fa32f5b68
+x %s 11 = fffffffffffffffd
 ~x = 56ad4183fcf7128a
 x & y = a802280c02084960
 x | y = f95fbf7edfdfedf5
@@ -3612,6 +5052,18 @@ x /u y2 = 64f253db1
 x %u y2 = 1b1f8b24
 x /s y3 = ffffffff34f67dfd
 x %s y3 = ffffffffe00e78a0
+x /u 3 = 4bcddb50788f348f
+x %u 3 = 2
+x /s 3 = f67885fb2339df3b
+x %s 3 = fffffffffffffffe
+x /u 5 = 2d7b8396aebc52bc
+x %u 5 = 3
+x /s 5 = fa4850637b891f8a
+x %s 5 = fffffffffffffffd
+x /u 11 = 14ac81a1953e5427
+x %u 11 = 2
+x /s 11 = fd66b02d38270e56
+x %s 11 = fffffffffffffffd
 ~x = 1c966e0e96526250
 x & y = 200910f161010802
 x | y = e76bf7fb6fad9fbf
@@ -3642,6 +5094,18 @@ x /u y2 = 7bb650b1
 x %u y2 = b51254f9
 x /s y3 = fffffff6f29b761c
 x %s y3 = 33e2279
+x /u 3 = 2725c483ee5a66d3
+x %u 3 = 0
+x /s 3 = 2725c483ee5a66d3
+x %s 3 = 0
+x /u 5 = 177d0f825bcfd74b
+x %u 5 = 2
+x /s 5 = 177d0f825bcfd74b
+x %s 5 = 2
+x /u 11 = aad359858473350
+x %u 11 = 9
+x /s 11 = aad359858473350
+x %s 11 = 9
 ~x = 8a8eb27434f0cb86
 x & y = 710005808a080010
 x | y = f777ff8beb8ff5fd
@@ -3672,6 +5136,18 @@ x /u y2 = a1fbf096
 x %u y2 = 8c67f383
 x /s y3 = 4ecae6205
 x %s y3 = fffffffff5e0333b
+x /u 3 = 315fd6992189fc1b
+x %u 3 = 2
+x /s 3 = dc0a8143cc34a6c7
+x %s 3 = fffffffffffffffe
+x /u 5 = 1d9fe728adb930dd
+x %u 5 = 2
+x /s 5 = ea6cb3f57a85fdab
+x %s 5 = fffffffffffffffc
+x /u 11 = d773a86da99fef0
+x %u 11 = 3
+x /s 11 = f63169127d82b91f
+x %s 11 = fffffffffffffffe
 ~x = 6be07c349b620bac
 x & y = 80180008408da042
 x | y = fe1f93fbffbff4f7
@@ -3702,6 +5178,18 @@ x /u y2 = 30cdb0a56
 x %u y2 = ad1e409
 x /s y3 = 30cdb0a56
 x %s y3 = ad1e409
+x /u 3 = 2834594c36a7a13f
+x %u 3 = 0
+x /s 3 = 2834594c36a7a13f
+x %s 3 = 0
+x /u 5 = 181f68c753fe2d8c
+x %u 5 = 1
+x /s 5 = 181f68c753fe2d8c
+x %s 5 = 1
+x /u 11 = af70114c91671cb
+x %u 11 = 4
+x /s 11 = af70114c91671cb
+x %s 11 = 4
 ~x = 8762f41b5c091c42
 x & y = 20880284a1c04088
 x | y = 7f9fefeeefffefbd
@@ -3732,6 +5220,18 @@ x /u y2 = 3274b0b2
 x %u y2 = 9b290b19
 x /s y3 = fffffffc3766d779
 x %s y3 = 5c46e48
+x /u 3 = ffc62752ea32467
+x %u 3 = 2
+x /s 3 = ffc62752ea32467
+x %s 3 = 2
+x /u 5 = 9976e464f2eaf71
+x %u 5 = 2
+x /s 5 = 9976e464f2eaf71
+x %s 5 = 2
+x /u 11 = 45c1ada23fdf2a7
+x %u 11 = a
+x /s 11 = 45c1ada23fdf2a7
+x %s 11 = a
 ~x = d00ad8a0741692c8
 x & y = 2351270701a06c32
 x | y = fff727ffcbe9fdff
@@ -3762,6 +5262,18 @@ x /u y2 = 68ee956da
 x %u y2 = 135a2859
 x /s y3 = fffffffe50888709
 x %s y3 = ffffffffe4ade05d
+x /u 3 = 43e30e669be75515
+x %u 3 = 2
+x /s 3 = ee8db9114691ffc1
+x %s 3 = fffffffffffffffe
+x /u 5 = 28bb6f0a5d8acca6
+x %u 5 = 3
+x /s 5 = f5883bd72a579974
+x %s 5 = fffffffffffffffd
+x /u 11 = 1283be1bfbf945c0
+x %u 11 = 1
+x /s 11 = fb3deca79ee1ffef
+x %s 11 = fffffffffffffffc
 ~x = 3456d4cc2c4a00be
 x & y = b09080050919e00
 x | y = dfadfff7d7fffffd
@@ -3792,6 +5304,18 @@ x /u y2 = 16ebd54de
 x %u y2 = b47cbf9
 x /s y3 = 16ebd54de
 x %s y3 = b47cbf9
+x /u 3 = 184674b358648ec9
+x %u 3 = 0
+x /s 3 = 184674b358648ec9
+x %s 3 = 0
+x /u 5 = e90ac6b9b6f88df
+x %u 5 = 0
+x /s 5 = e90ac6b9b6f88df
+x %s 5 = 0
+x /u 11 = 69eda025dece11f
+x %u 11 = 6
+x /s 11 = 69eda025dece11f
+x %s 11 = 6
 ~x = b72ca1e5f6d253a4
 x & y = d15e1a0124a04a
 x | y = 7ad7df5f99effe5f
@@ -3822,6 +5346,18 @@ x /u y2 = 6ea800f5e
 x %u y2 = a23e0b1
 x /s y3 = fffffffda06520cf
 x %s y3 = ffffffffe848911b
+x /u 3 = 3f87dbe9ca339901
+x %u 3 = 2
+x /s 3 = ea32869474de43ad
+x %s 3 = fffffffffffffffe
+x /u 5 = 261e50bf7952289a
+x %u 5 = 3
+x /s 5 = f2eb1d8c461ef568
+x %s 5 = fffffffffffffffd
+x /u 11 = 1153991137255846
+x %u 11 = 3
+x /s 11 = fa0dc79cda0e1275
+x %s 11 = fffffffffffffffe
 ~x = 41686c42a16534fa
 x & y = 1a8691b408188800
 x | y = bf9fdfff5fbfef35
@@ -3852,6 +5388,18 @@ x /u y2 = c46523b0
 x %u y2 = 22e57ccf
 x /s y3 = ffffffff181acd99
 x %s y3 = 84d7ca
+x /u 3 = 237216428d33873f
+x %u 3 = 2
+x /s 3 = 237216428d33873f
+x %s 3 = 2
+x /u 5 = 154473c187ebb78c
+x %u 5 = 3
+x /s 5 = 154473c187ebb78c
+x %s 5 = 3
+x /u 11 = 9aac040b225536e
+x %u 11 = 5
+x /s 11 = 9aac040b225536e
+x %s 11 = 5
 ~x = 95a9bd3858656a40
 x & y = a140085a20894a2
 x | y = eade56ffff9a95ff
@@ -3882,6 +5430,18 @@ x /u y2 = 9c21e58a
 x %u y2 = 1d492637
 x /s y3 = 9c21e58a
 x %s y3 = 1d492637
+x /u 3 = 17280248a41a9903
+x %u 3 = 0
+x /s 3 = 17280248a41a9903
+x %s 3 = 0
+x /u 5 = de4ce2b95a98f01
+x %u 5 = 4
+x /s 5 = de4ce2b95a98f01
+x %s 5 = 4
+x /u 11 = 650bacdfe35cca3
+x %u 11 = 8
+x /s 11 = 650bacdfe35cca3
+x %s 11 = 8
 ~x = ba87f92613b034f6
 x & y = 41600251ec448800
 x | y = 75ff4fddef6febed
@@ -3912,6 +5472,18 @@ x /u y2 = c4213692
 x %u y2 = cc1104f
 x /s y3 = c4213692
 x %s y3 = cc1104f
+x /u 3 = 350dbb8fd876f21
+x %u 3 = 0
+x /s 3 = 350dbb8fd876f21
+x %s 3 = 0
+x /u 5 = 1fd50a231b7a913
+x %u 5 = 4
+x /s 5 = 1fd50a231b7a913
+x %s 5 = 4
+x /u 11 = e781be16994cda
+x %u 11 = 5
+x /s 11 = e781be16994cda
+x %s 11 = 5
 ~x = f60d6cd50769b29c
 x & y = 8f2902aa8960822
 x | y = dfbf33af8d67df7
@@ -3942,6 +5514,18 @@ x /u y2 = 18af89756
 x %u y2 = 2bc2aae5
 x /s y3 = 240bce76
 x %s y3 = ffffffffefb31365
+x /u 3 = 50ae5f06a70a966f
+x %u 3 = 0
+x /s 3 = fb5909b151b5411a
+x %s 3 = ffffffffffffffff
+x /u 5 = 30689f6a64398d75
+x %u 5 = 4
+x /s 5 = fd356c3731065a43
+x %s 5 = fffffffffffffffe
+x /u 11 = 160102a4b9316ed8
+x %u 11 = 5
+x /s 11 = febb31305c1a2907
+x %s 11 = 0
 ~x = df4e2ec0ae03cb2
 x & y = 9001101055110048
 x | y = feeb5d9ff7bfcbdd
@@ -3972,6 +5556,18 @@ x /u y2 = 23f5eca36
 x %u y2 = 5804c9f
 x /s y3 = ffffffffe9ec23f1
 x %s y3 = ffffffff93aae1cb
+x /u 3 = 522e145f28e067c2
+x %u 3 = 1
+x /s 3 = fcd8bf09d38b126d
+x %s 3 = 0
+x /u 5 = 314ed905e5537174
+x %u 5 = 3
+x /s 5 = fe1ba5d2b2203e42
+x %s 5 = fffffffffffffffd
+x /u 11 = 1669a8770b25edc0
+x %u 11 = 7
+x /s 11 = ff23d702ae0ea7f0
+x %s 11 = fffffffffffffff7
 ~x = 975c2e2855ec8b8
 x & y = 6480391c40213142
 x | y = ffbb7d3dfafd77cf
@@ -4002,6 +5598,18 @@ x /u y2 = 209ed682d
 x %u y2 = 2780177c
 x /s y3 = ffffffffa02bad7e
 x %s y3 = ffffffffefe191e3
+x /u 3 = 481894a813d33d45
+x %u 3 = 2
+x /s 3 = f2c33f52be7de7f1
+x %s 3 = fffffffffffffffe
+x /u 5 = 2b41f2cb3f1857f6
+x %u 5 = 3
+x /s 5 = f80ebf980be524c4
+x %s 5 = fffffffffffffffd
+x /u 11 = 13a99ce8056827fb
+x %u 11 = 8
+x /s 11 = fc63cb73a850e22b
+x %s 11 = fffffffffffffff8
 ~x = 27b64207c486482e
 x & y = 480009c812208000
 x | y = fa5ffdf9fffbb7dd
@@ -4032,6 +5640,18 @@ x /u y2 = 21e776484
 x %u y2 = 1226152f
 x /s y3 = ffffffffc5acab53
 x %s y3 = ffffffffdfdae8ae
+x /u 3 = 4d0c90b82228a7ce
+x %u 3 = 1
+x /s 3 = f7b73b62ccd35279
+x %s 3 = 0
+x /u 5 = 2e3abd3b47b1fe48
+x %u 5 = 3
+x /s 5 = fb078a08147ecb16
+x %s 5 = fffffffffffffffd
+x /u 11 = 15036d497dadff38
+x %u 11 = 3
+x /s 11 = fdbd9bd52096b967
+x %s 11 = fffffffffffffffe
 ~x = 18da4dd799860894
 x & y = 650522284059140a
 x | y = ef35bbaf67fdf77f
@@ -4062,6 +5682,18 @@ x /u y2 = 7c0e5692
 x %u y2 = 41025c7b
 x /s y3 = 7c0e5692
 x %s y3 = 41025c7b
+x /u 3 = f80114c9c91a431
+x %u 3 = 2
+x /s 3 = f80114c9c91a431
+x %s 3 = 2
+x /u 5 = 94cd72df78a95b7
+x %u 5 = 2
+x /s 5 = 94cd72df78a95b7
+x %s 5 = 2
+x /u 11 = 43a33437084cfb0
+x %u 11 = 5
+x /s 11 = 43a33437084cfb0
+x %s 11 = 5
 ~x = d17fcc1a2a4b136a
 x & y = e8012a510040080
 x | y = 7ff573e5fdfcee95
@@ -4092,6 +5724,18 @@ x /u y2 = 14d521718
 x %u y2 = 4c657d7
 x /s y3 = 3b4ec343
 x %s y3 = ffffffffcaaf32b0
+x /u 3 = 4fc13fa657807b45
+x %u 3 = 0
+x /s 3 = fa6bea51022b25f0
+x %s 3 = ffffffffffffffff
+x /u 5 = 2fda5963ce19e38f
+x %u 5 = 4
+x /s 5 = fca726309ae6b05d
+x %s 5 = fffffffffffffffe
+x /u 11 = 15c0572d5daead41
+x %u 11 = 4
+x /s 11 = fe7a85b900976770
+x %s 11 = ffffffffffffffff
 ~x = 10bc410cf97e8e30
 x & y = a74320f104013182
 x | y = ffc3bef7079973ff
@@ -4122,6 +5766,18 @@ x /u y2 = 21584e541
 x %u y2 = 263b3f29
 x /s y3 = fffffffe66636700
 x %s y3 = fffffffff6e1d599
+x /u 3 = 3045ac776eb1a1dd
+x %u 3 = 2
+x /s 3 = daf05722195c4c89
+x %s 3 = fffffffffffffffe
+x /u 5 = 1cf69aae0f37611e
+x %u 5 = 3
+x /s 5 = e9c3677adc042dec
+x %s 5 = fffffffffffffffd
+x /u 11 = d2a464f1e3071f6
+x %u 11 = 7
+x /s 11 = f5e474dac1192c26
+x %s 11 = fffffffffffffff7
 ~x = 6f2efa99b3eb1a66
 x & y = 5000604004c410
 x | y = d5fddf76cf17e5bd
@@ -4152,6 +5808,18 @@ x /u y2 = 364afcce3
 x %u y2 = f56632d
 x /s y3 = 364afcce3
 x %s y3 = f56632d
+x /u 3 = 29903afe3eca437b
+x %u 3 = 2
+x /s 3 = 29903afe3eca437b
+x %s 3 = 2
+x /u 5 = 18f0236558dfc217
+x %u 5 = 0
+x /s 5 = 18f0236558dfc217
+x %s 5 = 0
+x /u 11 = b55e18b2865b550
+x %u 11 = 3
+x /s 11 = b55e18b2865b550
+x %s 11 = 3
 ~x = 834f4f0543a1358c
 x & y = 24b0b082104e0002
 x | y = 7cbef4fabf7feef7
@@ -4182,6 +5850,18 @@ x /u y2 = 2be74f23
 x %u y2 = 27781c66
 x /s y3 = fffffffbf88ea18f
 x %s y3 = 1a482a
+x /u 3 = e097ab22faf2249
+x %u 3 = 2
+x /s 3 = e097ab22faf2249
+x %s 3 = 2
+x /u 5 = 86c166ae9691492
+x %u 5 = 3
+x /s 5 = 86c166ae9691492
+x %s 5 = 3
+x /u 11 = 3d40a3098a4209f
+x %u 11 = 8
+x /s 11 = 3d40a3098a4209f
+x %s 11 = 8
 ~x = d5e38fe970f29922
 x & y = 200c50140d092008
 x | y = ff9c769fbf6f7ffd
@@ -4212,6 +5892,18 @@ x /u y2 = 1e3f46921
 x %u y2 = 59fa719a
 x /s y3 = ffffffff79b4afc3
 x %s y3 = ffffffffe0043b40
+x /u 3 = 42cc27abb2f6771d
+x %u 3 = 0
+x /s 3 = ed76d2565da121c8
+x %s 3 = ffffffffffffffff
+x /u 5 = 281417cd6b60adde
+x %u 5 = 1
+x /s 5 = f4e0e49a382d7aab
+x %s 5 = 0
+x /u 11 = 1237adba76a04f07
+x %u 11 = a
+x /s 11 = faf1dc4619890937
+x %s 11 = fffffffffffffffa
 ~x = 379b88fce71c9aa8
 x & y = 4800230110416012
 x | y = ea64ff1ffeeb7fdf
@@ -4242,6 +5934,18 @@ x /u y2 = 225392f08
 x %u y2 = 3be1c661
 x /s y3 = fffffffe8297e39a
 x %s y3 = fffffffff93b6ee1
+x /u 3 = 325c4e6498977c20
+x %u 3 = 1
+x /s 3 = dd06f90f434226cb
+x %s 3 = 0
+x /u 5 = 1e37623c5b8e1746
+x %u 5 = 3
+x /s 5 = eb042f09285ae414
+x %s 5 = fffffffffffffffd
+x /u 11 = dbc156140e37ef1
+x %u 11 = 6
+x /s 11 = f67643ece3cc3921
+x %s 11 = fffffffffffffff6
 ~x = 68eb14d236398b9e
 x & y = 600c90049421440
 x | y = d77fefedebff757d
@@ -4272,6 +5976,18 @@ x /u y2 = 32bcb4e0b
 x %u y2 = 13cff1ba
 x /s y3 = 32bcb4e0b
 x %s y3 = 13cff1ba
+x /u 3 = 22aee1ee38ba4cd3
+x %u 3 = 2
+x /s 3 = 22aee1ee38ba4cd3
+x %s 3 = 2
+x /u 5 = 14cf545bbba2fae5
+x %u 5 = 2
+x /s 5 = 14cf545bbba2fae5
+x %s 5 = 2
+x /u 11 = 975836f83d5b7dc
+x %u 11 = 7
+x /s 11 = 975836f83d5b7dc
+x %s 11 = 7
 ~x = 97f35a3555d11984
 x & y = 200ca1c28a04006a
 x | y = 68cfe7ebefbeefff
@@ -4302,6 +6018,18 @@ x /u y2 = 2ed78e4eb
 x %u y2 = 356cebb8
 x /s y3 = ffffffff3a97a9d7
 x %s y3 = fffffffff8b9f944
+x /u 3 = 438af87d1c4ac60c
+x %u 3 = 1
+x /s 3 = ee35a327c6f570b7
+x %s 3 = 0
+x /u 5 = 28869517ddc676d4
+x %u 5 = 1
+x /s 5 = f55361e4aa9343a1
+x %s 5 = 0
+x /u 11 = 126bb8221efd1ebd
+x %u 11 = 6
+x /s 11 = fb25e6adc1e5d8ed
+x %s 11 = fffffffffffffff6
 ~x = 355f1688ab1fadda
 x & y = 4020680754004000
 x | y = cfb6ed77f7ff5ef5
@@ -4332,6 +6060,18 @@ x /u y2 = 28a1bbf24
 x %u y2 = 799b1b7
 x /s y3 = fffffffe040371a9
 x %s y3 = ffffffffc98b7515
+x /u 3 = 2fe719b1215bbb4a
+x %u 3 = 1
+x /s 3 = da91c45bcc0665f5
+x %s 3 = 0
+x /u 5 = 1cbddc371403d6c6
+x %u 5 = 1
+x /s 5 = e98aa903e0d0a393
+x %s 5 = 0
+x /u 11 = d107b5eda8d619f
+x %u 11 = a
+x /s 11 = f5caa9ea7d761bcf
+x %s 11 = fffffffffffffffa
 ~x = 704ab2ec9becce20
 x & y = 894481244032082
 x | y = bfb7edbb6f5ff7df
@@ -4362,6 +6102,18 @@ x /u y2 = 13ff0e2ae
 x %u y2 = 476c04b9
 x /s y3 = 13ff0e2ae
 x %s y3 = 476c04b9
+x /u 3 = 1ff4b575c47d2c0d
+x %u 3 = 2
+x /s 3 = 1ff4b575c47d2c0d
+x %s 3 = 2
+x /u 5 = 132c6ce042b180d5
+x %u 5 = 0
+x /s 5 = 132c6ce042b180d5
+x %s 5 = 0
+x /u 11 = 8b71a3764222349
+x %u 11 = 6
+x /s 11 = 8b71a3764222349
+x %s 11 = 6
 ~x = a021df9eb2887bd6
 x & y = 4c94000045570000
 x | y = 5fff7369fff797ad
@@ -4392,6 +6144,18 @@ x /u y2 = 23b3ba758
 x %u y2 = 279118f3
 x /s y3 = fffffffe9e07f55d
 x %s y3 = ffffffffd0bd48a5
+x /u 3 = 34af9fbbece823d6
+x %u 3 = 1
+x /s 3 = df5a4a669792ce81
+x %s 3 = 0
+x /u 5 = 1f9c930a5af1af1a
+x %u 5 = 1
+x /s 5 = ec695fd727be7be7
+x %s 5 = 0
+x /u 11 = e5e7161cc3f4f97
+x %u 11 = 6
+x /s 11 = f7189fed6f2809c7
+x %s 11 = fffffffffffffff6
 ~x = 61f120cc3947947c
 x & y = 6049232c2206002
 x | y = dedfdf77deff6fd7
@@ -4422,6 +6186,18 @@ x /u y2 = 45edad94
 x %u y2 = a1dd3be1
 x /s y3 = fffffffb12493a09
 x %s y3 = d41d9ce
+x /u 3 = 1615de9b317844cf
+x %u 3 = 0
+x /s 3 = 1615de9b317844cf
+x %s 3 = 0
+x /u 5 = d40525d1dae8faf
+x %u 5 = 2
+x /s 5 = d40525d1dae8faf
+x %s 5 = 2
+x /u 11 = 605f6e481dafb7e
+x %u 11 = 3
+x /s 11 = 605f6e481dafb7e
+x %s 11 = 3
 ~x = bdbe642e6b973192
 x & y = 420083418428cc68
 x | y = f2cf9bf79decdf7d
@@ -4452,6 +6228,18 @@ x /u y2 = 3048d2c3e
 x %u y2 = 7ddbd3f
 x /s y3 = fffffffe386a7a90
 x %s y3 = fffffffff6bdc2a7
+x /u 3 = 35adadd00d2afd22
+x %u 3 = 1
+x /s 3 = e058587ab7d5a7cd
+x %s 3 = 0
+x /u 5 = 203501e33b19cb14
+x %u 5 = 3
+x /s 5 = ed01ceb007e697e2
+x %s 5 = fffffffffffffffd
+x /u 11 = ea3bb0a3222ff37
+x %u 11 = a
+x /s 11 = f75de995d50bb967
+x %s 11 = fffffffffffffffa
 ~x = 5ef6f68fd87f0898
 x & y = 2108086026801762
 x | y = b55db97c77c2f76f
@@ -4482,6 +6270,18 @@ x /u y2 = c7279a22
 x %u y2 = cb0da98f
 x /s y3 = 361b5597a
 x %s y3 = fffffffffb948337
+x /u 3 = 3cb93302689c66fb
+x %u 3 = 0
+x /s 3 = e763ddad134711a6
+x %s 3 = ffffffffffffffff
+x /u 5 = 246f1e9b0b910a96
+x %u 5 = 3
+x /s 5 = f13beb67d85dd764
+x %s 5 = fffffffffffffffd
+x /u 11 = 108f998c4b1361e7
+x %u 11 = 4
+x /s 11 = f949c817edfc1c16
+x %s 11 = ffffffffffffffff
 ~x = 49d466f8c62acb0e
 x & y = a22a8801014014a0
 x | y = fe2bffa77bff7efd
@@ -4512,6 +6312,18 @@ x /u y2 = 9ec1e9af
 x %u y2 = cf1df113
 x /s y3 = 68deaf7ef9
 x %s y3 = ffffffffffdef4c3
+x /u 3 = 34b9f12deab9d32e
+x %u 3 = 1
+x /s 3 = df649bd895647dd9
+x %s 3 = 0
+x /u 5 = 1fa2c3e859a2b1e8
+x %u 5 = 3
+x /s 5 = ec6f90b5266f7eb6
+x %s 5 = fffffffffffffffd
+x /u 11 = e6141c6b4613998
+x %u 11 = 3
+x /s 11 = f71b70525749f3c7
+x %s 11 = fffffffffffffffe
 ~x = 61d22c763fd28674
 x & y = 9e0111084008518a
 x | y = ff3df789d0bdfbbf
@@ -4542,6 +6354,18 @@ x /u y2 = 14b83ddb43
 x %u y2 = 7bd891d
 x /s y3 = fffffffe54d4c750
 x %s y3 = fffffffff8ae0935
+x /u 3 = 4ef92cb7884ca93c
+x %u 3 = 1
+x /s 3 = f9a3d76232f753e7
+x %s 3 = 0
+x /u 5 = 2f624e07b82dff24
+x %u 5 = 1
+x /s 5 = fc2f1ad484facbf1
+x %s 5 = 0
+x /u 11 = 1589c6609989456d
+x %u 11 = 6
+x /s 11 = fe43f4ec3c71ff9d
+x %s 11 = fffffffffffffff6
 ~x = 131479d9671a044a
 x & y = 86b040008048b20
 x | y = efefbfaebcedfbb5
@@ -4572,6 +6396,18 @@ x /u y2 = 6e847dbc
 x %u y2 = 63938b7
 x /s y3 = ffffffff7fb9c9d5
 x %s y3 = 8979c75
+x /u 3 = 13ca0e8122c0474f
+x %u 3 = 2
+x /s 3 = 13ca0e8122c0474f
+x %s 3 = 2
+x /u 5 = bdfa24d7b402ac9
+x %u 5 = 2
+x /s 5 = bdfa24d7b402ac9
+x %s 5 = 2
+x /u 11 = 565a6dd669187cf
+x %u 11 = a
+x /s 11 = 565a6dd669187cf
+x %s 11 = a
 ~x = c4a1d47c97bf2a10
 x & y = 904228268008542
 x | y = bbdeaf93ed49fdff
@@ -4602,6 +6438,18 @@ x /u y2 = 9a4aab1a
 x %u y2 = 8460af0b
 x /s y3 = 4ce035bf5
 x %s y3 = fffffffff8cc5e2a
+x /u 3 = 2e915ece37f03793
+x %u 3 = 0
+x /s 3 = d93c0978e29ae23e
+x %s 3 = ffffffffffffffff
+x /u 5 = 1bf0d27bbb29baf1
+x %u 5 = 4
+x /s 5 = e8bd9f4887f687bf
+x %s 5 = fffffffffffffffe
+x /u 11 = cb34866c9700f28
+x %u 11 = 1
+x /s 11 = f56d76f26c58c957
+x %s 11 = fffffffffffffffc
 ~x = 744be395582f5946
 x & y = 83800062a7508690
 x | y = efffbffbeff7b6fd
@@ -4632,6 +6480,18 @@ x /u y2 = 6cd85af3
 x %u y2 = 21606d91
 x /s y3 = fffffffd4a66f1cd
 x %s y3 = 6f4d315
+x /u 3 = 1f5c41f0b436badb
+x %u 3 = 2
+x /s 3 = 1f5c41f0b436badb
+x %s 3 = 2
+x /u 5 = 12d0f45d38eda350
+x %u 5 = 3
+x /s 5 = 12d0f45d38eda350
+x %s 5 = 3
+x /u 11 = 88d8658eb54be99
+x %u 11 = 0
+x /s 11 = 88d8658eb54be99
+x %s 11 = 0
 ~x = a1eb3a2de35bcf6c
 x & y = 5c0485521ca03002
 x | y = df56cdf65deff8b7
@@ -4662,6 +6522,18 @@ x /u y2 = 9e37e46d
 x %u y2 = 276a9058
 x /s y3 = fffffffe62f7568d
 x %s y3 = 3a458b38
+x /u 3 = 2621e032155e5354
+x %u 3 = 1
+x /s 3 = 2621e032155e5354
+x %s 3 = 1
+x /u 5 = 16e1201e0cd231ff
+x %u 5 = 2
+x /s 5 = 16e1201e0cd231ff
+x %s 5 = 2
+x /u 11 = a66546ac00273d1
+x %u 11 = 2
+x /s 11 = a66546ac00273d1
+x %s 11 = 2
 ~x = 8d9a5f69bfe50602
 x & y = 3000a010000af1c8
 x | y = fb7da79f7a7afdfd
@@ -4692,6 +6564,18 @@ x /u y2 = 89be8881
 x %u y2 = 3286ec30
 x /s y3 = ffffffff318b3773
 x %s y3 = 41b7412
+x /u 3 = 1b8a516de883a47d
+x %u 3 = 0
+x /s 3 = 1b8a516de883a47d
+x %s 3 = 0
+x /u 5 = 108630db8b822f7e
+x %u 5 = 1
+x /s 5 = 108630db8b822f7e
+x %s 5 = 1
+x /u 11 = 782d063cb0ca139
+x %u 11 = 4
+x /s 11 = 782d063cb0ca139
+x %s 11 = 4
 ~x = ad610bb646751288
 x & y = 108c644108804832
 x | y = db9ff5cfbbeeed7f
@@ -4722,6 +6606,18 @@ x /u y2 = fca32bce
 x %u y2 = 19279bff
 x /s y3 = 111f23d93
 x %s y3 = ffffffffe9244e4c
+x /u 3 = 46ec66cc210a532b
+x %u 3 = 0
+x /s 3 = f1971176cbb4fdd6
+x %s 3 = ffffffffffffffff
+x /u 5 = 2a8dd747470631e6
+x %u 5 = 3
+x /s 5 = f75aa41413d2feb4
+x %s 5 = fffffffffffffffd
+x /u 11 = 1357bef1da772df4
+x %u 11 = 5
+x /s 11 = fc11ed7d7d5fe823
+x %s 11 = 0
 ~x = 2b3acb9b9ce1067e
 x & y = d480300441145980
 x | y = d7df357767bffbfd
@@ -4752,6 +6648,18 @@ x /u y2 = 24340b83f
 x %u y2 = 41884ad8
 x /s y3 = ffffffff68c95c6b
 x %s y3 = ffffffffb854355c
+x /u 3 = 43ab247183879033
+x %u 3 = 2
+x /s 3 = ee55cf1c2e323adf
+x %s 3 = fffffffffffffffe
+x /u 5 = 2899e2aa821e2352
+x %u 5 = 1
+x /s 5 = f566af774eeaf01f
+x %s 5 = 0
+x /u 11 = 12747e4d80f66d25
+x %u 11 = 4
+x /s 11 = fb2eacd923df2754
+x %s 11 = ffffffffffffffff
 ~x = 34fe92ab75694f64
 x & y = 490141548290308a
 x | y = dbb7fd7debbef19f
@@ -4782,6 +6690,18 @@ x /u y2 = f958dab3
 x %u y2 = ecb4360b
 x /s y3 = 16380abc0
 x %s y3 = fffffffffebaf8c5
+x /u 3 = 4de81edf94efa317
+x %u 3 = 0
+x /s 3 = f892c98a3f9a4dc2
+x %s 3 = ffffffffffffffff
+x /u 5 = 2ebe78ec8c8fc841
+x %u 5 = 0
+x /s 5 = fb8b45b9595c950e
+x %s 5 = ffffffffffffffff
+x /u 11 = 153f4e3cfa12cf63
+x %u 11 = 4
+x /s 11 = fdf97cc89cfb8992
+x %s 11 = ffffffffffffffff
 ~x = 1647a361413116ba
 x & y = e9b0449e2888a940
 x | y = effcdcdefeeefd75
@@ -4812,6 +6732,18 @@ x /u y2 = ff8db266
 x %u y2 = cc4dce6f
 x /s y3 = 10cb8d59a
 x %s y3 = fffffffffdc42d8f
+x /u 3 = 524bd3e231be74aa
+x %u 3 = 1
+x /s 3 = fcf67e8cdc691f55
+x %s 3 = 0
+x /u 5 = 3160b254843f12cc
+x %u 5 = 3
+x /s 5 = fe2d7f21510bdf9a
+x %s 5 = fffffffffffffffd
+x /u 11 = 1671c56c3c1cab74
+x %u 11 = 3
+x /s 11 = ff2bf3f7df0565a3
+x %s 11 = fffffffffffffffe
 ~x = 91c84596ac4a200
 x & y = f641690005230822
 x | y = f7f3fbbe9ffbddff
@@ -4842,6 +6774,18 @@ x /u y2 = 13f341cd4
 x %u y2 = 3ea81d95
 x /s y3 = 13f341cd4
 x %s y3 = 3ea81d95
+x /u 3 = 23c2d779fce86f18
+x %u 3 = 1
+x /s 3 = 23c2d779fce86f18
+x %s 3 = 1
+x /u 5 = 1574e7af97bea90e
+x %u 5 = 3
+x /s 5 = 1574e7af97bea90e
+x %s 5 = 3
+x /u 11 = 9c0c667166defc0
+x %u 11 = 9
+x /s 11 = 9c0c667166defc0
+x %s 11 = 9
 ~x = 94b779920946b2b6
 x & y = 42080049e2884c00
 x | y = 7f4af6fdfeff4f6d
@@ -4872,6 +6816,18 @@ x /u y2 = c79a1999e
 x %u y2 = 8cb3bd5
 x /s y3 = fffffffc39559faa
 x %s y3 = fffffffffec068e9
+x /u 3 = 4181764beb21088b
+x %u 3 = 2
+x /s 3 = ec2c20f695cbb337
+x %s 3 = fffffffffffffffe
+x /u 5 = 274dad60c0470520
+x %u 5 = 3
+x /s 5 = f41a7a2d8d13d1ee
+x %s 5 = fffffffffffffffd
+x /u 11 = 11dd7d5a85f1bc83
+x %u 11 = 2
+x /s 11 = fa97abe628da76b2
+x %s 11 = fffffffffffffffd
 ~x = 3b7b9d1c3e9ce65c
 x & y = 4802261416119a2
 x | y = cfc4f2ebef6bdff7
@@ -4902,6 +6858,18 @@ x /u y2 = 373dc3a72
 x %u y2 = f3a74a9
 x /s y3 = fffffffca40c567c
 x %s y3 = ffffffffeb083c95
+x /u 3 = 2b406be27c6ef884
+x %u 3 = 1
+x /s 3 = d5eb168d2719a32f
+x %s 3 = 0
+x /u 5 = 19f373ee4aa8fb82
+x %u 5 = 3
+x /s 5 = e6c040bb1775c850
+x %s 5 = fffffffffffffffd
+x /u 11 = bcbc0550aa9e6af
+x %u 11 = 8
+x /s 11 = f485eee0ad92a0df
+x %s 11 = fffffffffffffff8
 ~x = 7e3ebc588ab31672
 x & y = 181000200488008
 x | y = a5d543a7fddeeb9d
@@ -4932,6 +6900,18 @@ x /u y2 = 3f82fa73
 x %u y2 = 22447773
 x /s y3 = 3f82fa73
 x %s y3 = 22447773
+x /u 3 = 81b55f36c1b6d2d
+x %u 3 = 0
+x /s 3 = 81b55f36c1b6d2d
+x %s 3 = 0
+x /u 5 = 4dd33920daa0e4e
+x %u 5 = 1
+x /s 5 = 4dd33920daa0e4e
+x %s 5 = 1
+x /u 11 = 236002b1d7bd7f5
+x %u 11 = 0
+x /s 11 = 236002b1d7bd7f5
+x %s 11 = 0
 ~x = e7adfe25bbadb878
 x & y = 2009800400502
 x | y = 7a5787dec4ff4f8f
@@ -4962,6 +6942,18 @@ x /u y2 = a8d5772
 x %u y2 = 2bbf7115
 x /s y3 = a8d5772
 x %s y3 = 2bbf7115
+x /u 3 = 1955730431eeb5b
+x %u 3 = 0
+x /s 3 = 1955730431eeb5b
+x %s 3 = 0
+x /u 5 = f334502845c069
+x %u 5 = 4
+x /s 5 = f334502845c069
+x %s 5 = 4
+x /u 11 = 6e8c246f658601
+x %u 11 = 6
+x /s 11 = 6e8c246f658601
+x %s 11 = 6
 ~x = fb3ffa6f36a33dee
 x & y = 50040400000
 x | y = 77fd57fee9fdcf5d
@@ -4992,6 +6984,18 @@ x /u y2 = a2d45f9b
 x %u y2 = 7184712
 x /s y3 = a2d45f9b
 x %s y3 = 7184712
+x /u 3 = 187cdc6afb43d939
+x %u 3 = 0
+x /s 3 = 187cdc6afb43d939
+x %s 3 = 0
+x /u 5 = eb1510cfd28b588
+x %u 5 = 3
+x /s 5 = eb1510cfd28b588
+x %s 5 = 3
+x /u 11 = 6adb07a4486de26
+x %u 11 = 9
+x /s 11 = 6adb07a4486de26
+x %s 11 = 9
 ~x = b6896abf0e347454
 x & y = 4176814080cb830a
 x | y = 7b7fb5dbf1ffebff
@@ -5022,6 +7026,18 @@ x /u y2 = 1056b28b9
 x %u y2 = 986cffaf
 x /s y3 = dab98c69
 x %s y3 = fffffffff99e128f
+x /u 3 = 4c147aad9bf6b39c
+x %u 3 = 1
+x /s 3 = f6bf255846a15e47
+x %s 3 = 0
+x /u 5 = 2da5e334f72d9ef7
+x %u 5 = 2
+x /s 5 = fa72b001c3fa6bc5
+x %s 5 = fffffffffffffffc
+x /u 11 = 14bfc45de4b7a559
+x %u 11 = 2
+x /s 11 = fd79f2e987a05f88
+x %s 11 = fffffffffffffffd
 ~x = 1bc28ff72c1be52a
 x & y = c400500011c002c0
 x | y = ffbf755efbecfbd5
@@ -5052,6 +7068,18 @@ x /u y2 = 1027d221e
 x %u y2 = e50c5a15
 x /s y3 = a31a1d6d
 x %s y3 = fffffffff9b9f758
+x /u 3 = 53ea3033c7d1435a
+x %u 3 = 1
+x /s 3 = fe94dade727bee05
+x %s 3 = 0
+x /u 5 = 3259501f117d8ecf
+x %u 5 = 4
+x /s 5 = ff261cebde4a5b9d
+x %s 5 = fffffffffffffffe
+x /u 11 = 16e2c753f0ad6f75
+x %u 11 = 8
+x /s 11 = ff9cf5df939629a5
+x %s 11 = fffffffffffffff8
 ~x = 4416f64a88c35f0
 x & y = f912001356324202
 x | y = fbfe9ebbd7fbfeff
@@ -5082,6 +7110,18 @@ x /u y2 = d967540f
 x %u y2 = 73d47f08
 x /s y3 = 14a5fa443
 x %s y3 = ffffffffb843c4bc
+x /u 3 = 2fb5882bc358d29d
+x %u 3 = 2
+x /s 3 = da6032d66e037d49
+x %s 3 = fffffffffffffffe
+x /u 5 = 1ca01e80a8687e5e
+x %u 5 = 3
+x /s 5 = e96ceb4d75354b2c
+x %s 5 = fffffffffffffffd
+x /u 11 = d02f697925e0ae5
+x %u 11 = 2
+x /s 11 = f5bd25233546c514
+x %s 11 = fffffffffffffffd
 ~x = 70df677cb5f58826
 x & y = 880080034a003150
 x | y = afa99d9f5a0a7ffd
@@ -5112,6 +7152,18 @@ x /u y2 = 1cc9cbb61
 x %u y2 = ba5245
 x /s y3 = ffffffff8f617990
 x %s y3 = fffffffff0d03ed3
+x /u 3 = 44918413ecd20ce6
+x %u 3 = 1
+x /s 3 = ef3c2ebe977cb791
+x %s 3 = 0
+x /u 5 = 29241c0bf47e07bd
+x %u 5 = 2
+x /s 5 = f5f0e8d8c14ad48b
+x %s 5 = fffffffffffffffc
+x /u 11 = 12b35291120abdb3
+x %u 11 = 2
+x /s 11 = fb6d811cb4f377e2
+x %s 11 = fffffffffffffffd
 ~x = 324b73c43989d94c
 x & y = 4010882a00060282
 x | y = fff7cd3fe7fe3ff7
@@ -5142,6 +7194,18 @@ x /u y2 = 10c2e2273
 x %u y2 = 6febbad1
 x /s y3 = e4b07a4a
 x %s y3 = ffffffffb4b2dcf5
+x /u 3 = 3dd259abc52289b4
+x %u 3 = 1
+x /s 3 = e87d04566fcd345f
+x %s 3 = 0
+x /u 5 = 2517cf670fe185d2
+x %u 5 = 3
+x /s 5 = f1e49c33dcae52a0
+x %s 5 = fffffffffffffffd
+x /u 11 = 10dc47004d096b5f
+x %u 11 = 8
+x /s 11 = f996758beff2258f
+x %s 11 = fffffffffffffff8
 ~x = 4688f2fcb09862e2
 x & y = b102050041608008
 x | y = b97fad876f779f7d
@@ -5172,6 +7236,18 @@ x /u y2 = f5e9880c
 x %u y2 = 3dce52bf
 x /s y3 = fffffffefdc6ec2b
 x %s y3 = 7611c611
+x /u 3 = 29fc78873a7801dd
+x %u 3 = 0
+x /s 3 = 29fc78873a7801dd
+x %s 3 = 0
+x /u 5 = 1931151defe19ab7
+x %u 5 = 4
+x /s 5 = 1931151defe19ab7
+x %s 5 = 4
+x /u 11 = b7366b0844f4653
+x %u 11 = 6
+x /s 11 = b7366b0844f4653
+x %s 11 = 6
 ~x = 820a966a5097fa68
 x & y = 12029902c480592
 x | y = fff56d97ff7965df
@@ -5202,6 +7278,18 @@ x /u y2 = f41ffd27
 x %u y2 = 70c5e7
 x /s y3 = f41ffd27
 x %s y3 = 70c5e7
+x /u 3 = 1c68ebd7642d2f8b
+x %u 3 = 0
+x /s 3 = 1c68ebd7642d2f8b
+x %s 3 = 0
+x /u 5 = 110bc0b46f4e4fb9
+x %u 5 = 4
+x /s 5 = 110bc0b46f4e4fb9
+x %s 5 = 4
+x /u 11 = 7bf862378696a0e
+x %u 11 = 7
+x /s 11 = 7bf862378696a0e
+x %s 11 = 7
 ~x = aac53c79d378715e
 x & y = 5120018608820280
 x | y = 5d7adbb6feb7febd
@@ -5232,6 +7320,18 @@ x /u y2 = 2db65f96
 x %u y2 = 5a639c65
 x /s y3 = ffffffff897f0ff8
 x %s y3 = 1c534bc3
+x /u 3 = afef025a6cf0393
+x %u 3 = 2
+x /s 3 = afef025a6cf0393
+x %s 3 = 2
+x /u 5 = 698f67cfdaf688b
+x %u 5 = 4
+x /s 5 = 698f67cfdaf688b
+x %s 5 = 4
+x /u 11 = 2ffb5dbb9212f85
+x %u 11 = 4
+x /s 11 = 2ffb5dbb9212f85
+x %s 11 = 4
 ~x = df032f8f0b92f544
 x & y = 20bcc020c02c082a
 x | y = b8fcfa71fdfd2bbf
@@ -5262,6 +7362,18 @@ x /u y2 = 14171ae1b
 x %u y2 = 2178d143
 x /s y3 = 14171ae1b
 x %s y3 = 2178d143
+x /u 3 = 129aeb72773a3021
+x %u 3 = 2
+x /s 3 = 129aeb72773a3021
+x %s 3 = 2
+x /u 5 = b29c077e122e9ad
+x %u 5 = 4
+x /s 5 = b29c077e122e9ad
+x %s 5 = 4
+x /u 11 = 512fa65093e6a37
+x %u 11 = 8
+x /s 11 = 512fa65093e6a37
+x %s 11 = 8
 ~x = c82f3da89a516f9a
 x & y = 2450820665809000
 x | y = 3ff3e7d777affe75
@@ -5292,6 +7404,18 @@ x /u y2 = 12e961017
 x %u y2 = 22af4b61
 x /s y3 = 12e961017
 x %s y3 = 22af4b61
+x /u 3 = 296c3b705c8908b5
+x %u 3 = 0
+x /s 3 = 296c3b705c8908b5
+x %s 3 = 0
+x /u 5 = 18da8a1037856b9f
+x %u 5 = 4
+x /s 5 = 18da8a1037856b9f
+x %s 5 = 4
+x /u 11 = b4c1035eab1025f
+x %u 11 = a
+x /s 11 = b4c1035eab1025f
+x %s 11 = a
 ~x = 83bb4daeea64e5e0
 x & y = 68008250158b1802
 x | y = 7d66fff31dbb7bdf
@@ -5322,6 +7446,18 @@ x /u y2 = 6e285728ab
 x %u y2 = c1193
 x /s y3 = ffffffb7c1013ab9
 x %s y3 = fffffffffed4da77
+x /u 3 = 3388e09be749b778
+x %u 3 = 1
+x /s 3 = de338b4691f46223
+x %s 3 = 0
+x /u 5 = 1eebb9f7245f6e15
+x %u 5 = 0
+x /s 5 = ebb886c3f12c3ae2
+x %s 5 = ffffffffffffffff
+x /u 11 = e0e0eb627ce494f
+x %u 11 = 4
+x /s 11 = f6c83d41cab7037e
+x %s 11 = ffffffffffffffff
 ~x = 65655e2c4a22d996
 x & y = 2008224500040
 x | y = 9bffebd3bdff7eed
@@ -5352,6 +7488,18 @@ x /u y2 = f00fdea7
 x %u y2 = 896e5ed0
 x /s y3 = 187a673b8
 x %s y3 = fffffffffa8e4fab
+x /u 3 = 479b769873df7296
+x %u 3 = 1
+x /s 3 = f24621431e8a1d41
+x %s 3 = 0
+x /u 5 = 2af6e0c1df1fab27
+x %u 5 = 0
+x /s 5 = f7c3ad8eabec77f4
+x %s 5 = ffffffffffffffff
+x /u 11 = 13877d6f656b7c57
+x %u 11 = 6
+x /s 11 = fc41abfb08543687
+x %s 11 = fffffffffffffff6
 ~x = 292d9c36a461a83c
 x & y = c41000c118040382
 x | y = f7d7ebdddbdfffd7
@@ -5382,6 +7530,18 @@ x /u y2 = 23effdd7
 x %u y2 = 272c2ddf
 x /s y3 = ffffffff8b8269ef
 x %s y3 = 39a9e8af
+x /u 3 = 927a57ae606b18f
+x %u 3 = 0
+x /s 3 = 927a57ae606b18f
+x %s 3 = 0
+x /u 5 = 57e30168a040422
+x %u 5 = 3
+x /s 5 = 57e30168a040422
+x %s 5 = 3
+x /u 11 = 27f2d21848d763e
+x %u 11 = 3
+x /s 11 = 27f2d21848d763e
+x %s 11 = 3
 ~x = e4890f8f4debeb52
 x & y = 324c060920014a8
 x | y = dbf6f9f2bff5f6bd
diff --git a/test/regression/int64.c b/test/regression/int64.c
index 0012216f..d9785e95 100644
--- a/test/regression/int64.c
+++ b/test/regression/int64.c
@@ -56,6 +56,18 @@ static void test1(u64 x, u64 y)
   y3 = ((s64)y) >> 32;
   printf("x /s y3 = %llx\n", safe_sdiv64(x, y3));
   printf("x %%s y3 = %llx\n", safe_smod64(x, y3));
+  printf("x /u 3 = %llx\n", x / 3);
+  printf("x %%u 3 = %llx\n", x % 3);
+  printf("x /s 3 = %llx\n", (s64)x / 3);
+  printf("x %%s 3 = %llx\n", (s64)x % 3);
+  printf("x /u 5 = %llx\n", x / 5);
+  printf("x %%u 5 = %llx\n", x % 5);
+  printf("x /s 5 = %llx\n", (s64)x / 5);
+  printf("x %%s 5 = %llx\n", (s64)x % 5);
+  printf("x /u 11 = %llx\n", x / 11);
+  printf("x %%u 11 = %llx\n", x % 11);
+  printf("x /s 11 = %llx\n", (s64)x / 11);
+  printf("x %%s 11 = %llx\n", (s64)x % 11);
   printf("~x = %llx\n", ~x);
   printf("x & y = %llx\n", x & y);
   printf("x | y = %llx\n", x | y);
author	Xavier Leroy <xavier.leroy@inria.fr>	2016-10-04 15:52:16 +0200
committer	Xavier Leroy <xavier.leroy@inria.fr>	2016-10-04 15:52:16 +0200
commit	d2af79a77ed2936ff0ed90cadf8e48637d774d4c (patch)
tree	09300943e12a98ae80598c79d455b31725271ead
parent	a44893028eb1dd434c68001234ad56d030205a8e (diff)
download	compcert-kvx-d2af79a77ed2936ff0ed90cadf8e48637d774d4c.tar.gz compcert-kvx-d2af79a77ed2936ff0ed90cadf8e48637d774d4c.zip