Optimize integer divisions by positive constants, turning them into

multiply-high and shifts.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

36 files changed, 2663 insertions, 182 deletions

diff --git a/.depend b/.depend
index 17db282..ca707a4 100644
--- a/.depend
+++ b/.depend
@@ -30,11 +30,13 @@ backend/Cminor.vo backend/Cminor.glob backend/Cminor.v.beautified: backend/Cmino
 $(ARCH)/Op.vo $(ARCH)/Op.glob $(ARCH)/Op.v.beautified: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo
 backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo
 $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)/SelectOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo
+backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
 backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo
-backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo
+backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo
 $(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
+backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo
 backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo
-backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectLongproof.vo
+backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo
 backend/Registers.vo backend/Registers.glob backend/Registers.v.beautified: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo
 backend/RTL.vo backend/RTL.glob backend/RTL.v.beautified: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo
 backend/RTLgen.vo backend/RTLgen.glob backend/RTLgen.v.beautified: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo
diff --git a/Changelog b/Changelog
index a7151c6..657cb03 100644
--- a/Changelog
+++ b/Changelog
@@ -1,6 +1,8 @@
 Development trunk:
 ==================
 
+- Optimize integer divisions by positive constants, turning them into
+  multiply-high and shifts.
 - Avoid double rounding issues in conversion from 64-bit integers
   to single-precision floats.
 - PowerPC: more efficient implementation of division on 64-bit integers.
diff --git a/Makefile b/Makefile
index 76938b4..1694457 100644
--- a/Makefile
+++ b/Makefile
@@ -75,8 +75,8 @@ COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \
 
 BACKEND=\
   Cminor.v Op.v CminorSel.v \
-  SelectOp.v SelectLong.v Selection.v \
-  SelectOpproof.v SelectLongproof.v Selectionproof.v \
+  SelectOp.v SelectDiv.v SelectLong.v Selection.v \
+  SelectOpproof.v SelectDivproof.v SelectLongproof.v Selectionproof.v \
   Registers.v RTL.v \
   RTLgen.v RTLgenspec.v RTLgenproof.v \
   Tailcall.v Tailcallproof.v \
diff --git a/arm/Asm.v b/arm/Asm.v
index 43a1435..76e8196 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -157,9 +157,11 @@ Inductive instruction : Type :=
   | Pstr: ireg -> ireg -> shift_addr -> instruction (**r int32 store *)
   | Pstrb: ireg -> ireg -> shift_addr -> instruction (**r int8 store *)
   | Pstrh: ireg -> ireg -> shift_addr -> instruction (**r int16 store *)
-  | Psdiv: ireg -> ireg -> ireg -> instruction      (**r signed division *)
+  | Psdiv: instruction                              (**r signed division *)
+  | Psmull: ireg -> ireg -> ireg -> ireg -> instruction (**r signed multiply long *)
   | Psub: ireg -> ireg -> shift_op -> instruction  (**r integer subtraction *)
-  | Pudiv: ireg -> ireg -> ireg -> instruction      (**r unsigned division *)
+  | Pudiv: instruction                             (**r unsigned division *)
+  | Pumull: ireg -> ireg -> ireg -> ireg -> instruction (**r unsigned multiply long *)
   (* Floating-point coprocessor instructions (VFP double scalar operations) *)
   | Pfcpyd: freg -> freg -> instruction             (**r float move *)
   | Pfabsd: freg -> freg -> instruction             (**r float absolute value *)
@@ -559,18 +561,28 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_store Mint8unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m
   | Pstrh r1 r2 sa => 
       exec_store Mint16unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m
-  | Psdiv rd r1 r2 =>
-      match Val.divs rs#r1 rs#r2 with
-      | Some v => Next (nextinstr (rs#rd <- v)) m
+  | Psdiv =>
+      match Val.divs rs#IR0 rs#IR1 with
+      | Some v => Next (nextinstr (rs#IR0 <- v
+                                     #IR1 <- Vundef #IR2 <- Vundef
+                                     #IR3 <- Vundef #IR12 <- Vundef)) m
       | None => Stuck
       end
+  | Psmull rdl rdh r1 r2 =>
+      Next (nextinstr (rs#rdl <- (Val.mul rs#r1 rs#r2)
+                         #rdh <- (Val.mulhs rs#r1 rs#r2))) m
   | Psub r1 r2 so =>  
       Next (nextinstr (rs#r1 <- (Val.sub rs#r2 (eval_shift_op so rs)))) m
-  | Pudiv rd r1 r2 =>
-      match Val.divu rs#r1 rs#r2 with
-      | Some v => Next (nextinstr (rs#rd <- v)) m
+  | Pudiv =>
+      match Val.divu rs#IR0 rs#IR1 with
+      | Some v => Next (nextinstr (rs#IR0 <- v
+                                     #IR1 <- Vundef #IR2 <- Vundef
+                                     #IR3 <- Vundef #IR12 <- Vundef)) m
       | None => Stuck
       end
+  | Pumull rdl rdh r1 r2 =>
+      Next (nextinstr (rs#rdl <- (Val.mul rs#r1 rs#r2)
+                         #rdh <- (Val.mulhu rs#r1 rs#r2))) m
   (* Floating-point coprocessor instructions *)
   | Pfcpyd r1 r2 =>
       Next (nextinstr (rs#r1 <- (rs#r2))) m
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 6645149..3707b7f 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -299,12 +299,22 @@ Definition transl_op
       OK (if negb (ireg_eq r r1) then Pmla r r1 r2 r3 :: k
           else if negb (ireg_eq r r2) then Pmla r r2 r1 r3 :: k
           else Pmla IR14 r1 r2 r3 :: Pmov r (SOreg IR14) :: k)
-  | Odiv, a1 :: a2 :: nil =>
+  | Omulhs, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psdiv r r1 r2 :: k)
-  | Odivu, a1 :: a2 :: nil =>
+      OK (Psmull IR14 r r1 r2 :: k)
+  | Omulhu, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pudiv r r1 r2 :: k)
+      OK (Pumull IR14 r r1 r2 :: k)
+  | Odiv, a1 :: a2 :: nil =>
+      assertion (mreg_eq res R0);
+      assertion (mreg_eq a1 R0);
+      assertion (mreg_eq a2 R1);
+      OK (Psdiv :: k)
+  | Odivu, a1 :: a2 :: nil =>
+      assertion (mreg_eq res R0);
+      assertion (mreg_eq a1 R0);
+      assertion (mreg_eq a2 R1);
+      OK (Pudiv :: k)
   | Oand, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (Pand r r1 (SOreg r2) :: k)
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index d77006a..21d2b73 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -942,11 +942,12 @@ Proof.
   eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
   intuition Simpl.
   (* divs *)
-  econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. 
-  intuition Simpl.
+Local Transparent destroyed_by_op.
+  econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
+  split. Simpl. simpl; intros. intuition Simpl. 
   (* divu *)
   econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
-  intuition Simpl.
+  split. Simpl. simpl; intros. intuition Simpl. 
   (* Oandimm *)
   generalize (andimm_correct x x0 i k rs m). 
   intros [rs' [A [B C]]]. 
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 9bf066b..caf0da6 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -112,6 +112,9 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Orsubshift s, I n1 :: I n2 :: nil => I(Int.sub (eval_static_shift s n2) n1)
   | Orsubimm n, I n1 :: nil => I (Int.sub n n1)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
+  | Omla, I n1 :: I n2 :: I n3 :: nil => I(Int.add (Int.mul n1 n2) n3)
+  | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2)
+  | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu n1 n2)
   | Odiv, I n1 :: I n2 :: nil =>
       if Int.eq n2 Int.zero then Unknown else
       if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
diff --git a/arm/Op.v b/arm/Op.v
index af3ccdb..fe97d36 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -82,6 +82,8 @@ Inductive operation : Type :=
   | Orsubimm: int -> operation          (**r [rd = n - r1] *)
   | Omul: operation                     (**r [rd = r1 * r2] *)
   | Omla: operation                     (**r [rd = r1 * r2 + r3] *)
+  | Omulhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omulhu: operation                   (**r [rd = high part of r1 * r2, unsigned] *)
   | Odiv: operation                     (**r [rd = r1 / r2] (signed) *)
   | Odivu: operation                    (**r [rd = r1 / r2] (unsigned) *)
   | Oand: operation                     (**r [rd = r1 & r2] *)
@@ -226,6 +228,8 @@ Definition eval_operation
   | Orsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1)
   | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
   | Omla, v1 :: v2 :: v3 :: nil => Some (Val.add (Val.mul v1 v2) v3)
+  | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
+  | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
   | Odiv, v1 :: v2 :: nil => Val.divs v1 v2
   | Odivu, v1 :: v2 :: nil => Val.divu v1 v2
   | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2)
@@ -319,6 +323,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Orsubimm _ => (Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
   | Omla => (Tint :: Tint :: Tint :: nil, Tint)
+  | Omulhs => (Tint :: Tint :: nil, Tint)
+  | Omulhu => (Tint :: Tint :: nil, Tint)
   | Odiv => (Tint :: Tint :: nil, Tint)
   | Odivu => (Tint :: Tint :: nil, Tint)
   | Oand => (Tint :: Tint :: nil, Tint)
@@ -396,6 +402,8 @@ Proof with (try exact I).
   destruct v0...
   destruct v0; destruct v1...
   destruct v0... destruct v1... destruct v2...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
   destruct v0; destruct v1; simpl in H0; inv H0.
     destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
   destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
@@ -823,6 +831,8 @@ Proof.
 
   inv H4; inv H2; simpl; auto.
   apply Values.val_add_inject; auto. inv H4; inv H2; 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 (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index d700326..c0e2687 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -599,14 +599,16 @@ let print_instruction oc = function
       fprintf oc "	strb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1
   | Pstrh(r1, r2, sa) ->
       fprintf oc "	strh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1
-  | Psdiv(r1, r2, r3) ->
-      assert (r1 = IR0 && r2 = IR0 && r3 = IR1);
+  | Psdiv ->
       fprintf oc "	bl	__aeabi_idiv\n"; 1
+  | Psmull(r1, r2, r3, r4) ->
+      fprintf oc "	smull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
   | Psub(r1, r2, so) ->
       fprintf oc "	sub	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
-  | Pudiv(r1, r2, r3) ->
-      assert (r1 = IR0 && r2 = IR0 && r3 = IR1);
+  | Pudiv ->
       fprintf oc "	bl	__aeabi_uidiv\n"; 1
+  | Pumull(r1, r2, r3, r4) ->
+      fprintf oc "	umull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
   (* Floating-point coprocessor instructions *)
   | Pfcpyd(r1, r2) ->
       fprintf oc "	fcpyd	%a, %a\n" freg r1 freg r2; 1
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index d81328b..4cd09d1 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -272,33 +272,20 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
                            Enil) :::
                  Enil))).
 
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-
-Definition mods := mod_aux Odiv.
-
-Definition divuimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => shruimm e l
-  | None   => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
-  end.
-
-Nondetfunction divu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => divuimm e1 n2
-  | _ => Eop Odivu (e1:::e2:::Enil)
-  end.
-
-Definition moduimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil)
-  | None   => mod_aux Odivu e (Eop (Ointconst n) Enil)
-  end.
-
-Nondetfunction modu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => moduimm e1 n2
-  | _ => mod_aux Odivu e1 e2
-  end.
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base := mod_aux Odiv.
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base := mod_aux Odivu.
+
+Definition shrximm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero
+  then e1
+  else Elet e1
+         (shrimm
+             (add (Eletvar O)
+                  (shruimm (shrimm (Eletvar O) (Int.repr 31))
+                           (Int.sub Int.iwordsize n2)))
+             n2).
 
 (** ** General shifts *)
 
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index a71ead7..9beb1ad 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -468,83 +468,103 @@ Proof.
   reflexivity.
 Qed.
 
-Theorem eval_divs:
+Theorem eval_divs_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divs x y = Some z ->
-  exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divs. exists z; split. EvalOp. auto.
+  intros. unfold divs_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_mods:
+Theorem eval_mods_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.mods x y = Some z ->
-  exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold mods. 
+  intros; unfold mods_base. 
   exploit Val.mods_divs; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divs); auto.
 Qed.
 
-Theorem eval_divuimm:
-  forall le n a x z,
-  eval_expr ge sp e m le a x ->
-  Val.divu x (Vint n) = Some z ->
-  exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v.
-Proof.
-  intros; unfold divuimm. 
-  destruct (Int.is_power2 n) eqn:?. 
-  replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto.
-  eapply Val.divu_pow2; eauto.
-  TrivialExists. 
-  econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
-Qed.
-
-Theorem eval_divu:
+Theorem eval_divu_base:
   forall le a x b y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divu x y = Some z ->
-  exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros until z. unfold divu; destruct (divu_match b); intros; InvEval.
-  eapply eval_divuimm; eauto.
-  TrivialExists. 
+  intros. unfold divu_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_moduimm:
-  forall le n a x z,
+Theorem eval_modu_base:
+  forall le a x b y z,
   eval_expr ge sp e m le a x ->
-  Val.modu x (Vint n) = Some z ->
-  exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v.
+  eval_expr ge sp e m le b y ->
+  Val.modu x y = Some z ->
+  exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold moduimm. 
-  destruct (Int.is_power2 n) eqn:?.
-  replace z with (Val.and x (Vint (Int.sub n Int.one))). TrivialExists.
-  eapply Val.modu_pow2; eauto.
+  intros; unfold modu_base. 
   exploit Val.modu_divu; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divu); auto.
-  EvalOp.
 Qed.
 
-Theorem eval_modu:
-  forall le a x b y z,
+Theorem eval_shrximm:
+  forall le a n x z,
   eval_expr ge sp e m le a x ->
-  eval_expr ge sp e m le b y ->
-  Val.modu x y = Some z ->
-  exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
+  Val.shrx x (Vint n) = Some z ->
+  exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
 Proof.
-  intros until y; unfold modu; case (modu_match b); intros; InvEval.
-  eapply eval_moduimm; eauto.
-  exploit Val.modu_divu; eauto. intros [v [A B]].
-  subst. econstructor; split; eauto.
-  apply eval_mod_aux with (semdivop := Val.divu); auto.
+  intros. unfold shrximm. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. exists x; split; auto. 
+  destruct x; simpl in H0; try discriminate.
+  destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
+  replace (Int.shrx i Int.zero) with i. auto. 
+  unfold Int.shrx, Int.divs. rewrite Int.shl_zero. 
+  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+- destruct x; simpl in H0; try discriminate.
+  destruct (Int.ltu n (Int.repr 31)) eqn:LT31; inv H0.
+  assert (A: eval_expr ge sp e m (Vint i :: le) (Eletvar 0) (Vint i))
+  by (constructor; auto).
+  exploit (eval_shrimm (Int.repr 31)). eexact A.
+  intros [v [B LD]]. simpl in LD. 
+  change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. 
+  simpl in LD; inv LD.
+  exploit (eval_shruimm (Int.sub Int.iwordsize n)). eexact B.
+  intros [v [C LD]]. simpl in LD.
+  assert (RANGE: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
+  {
+    generalize (Int.ltu_inv _ _ LT31). intros.
+    unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. 
+    rewrite Int.unsigned_repr. apply zlt_true.
+    assert (Int.unsigned n <> 0). 
+    { red; intros; elim H1. rewrite <- (Int.repr_unsigned n). rewrite H2; reflexivity. }
+    omega. 
+    change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
+    generalize Int.wordsize_max_unsigned; omega. 
+  }
+  rewrite RANGE in LD. inv LD. 
+  exploit eval_add. eexact A. eexact C. intros [v [D LD]].
+  simpl in LD. inv LD. 
+  exploit (eval_shrimm n). eexact D. intros [v [E LD]].
+  simpl in LD. 
+  assert (RANGE2: Int.ltu n Int.iwordsize = true).
+  {
+    generalize (Int.ltu_inv _ _ LT31). intros.
+    unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true.
+    change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
+    omega.
+  }
+  rewrite RANGE2 in LD. inv LD. 
+  econstructor; split. econstructor. eassumption. eexact E. 
+  rewrite Int.shrx_shr_2 by auto.
+  auto.
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
new file mode 100644
index 0000000..e60a97d
--- /dev/null
+++ b/backend/SelectDiv.vp
@@ -0,0 +1,156 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection for integer division and modulus *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Op.
+Require Import CminorSel.
+Require Import SelectOp.
+
+Open Local Scope cminorsel_scope.
+
+(** We try to turn divisions by a constant into a multiplication by
+  a pseudo-inverse of the divisor.  The approach is described in
+- Torbjörn Granlund, Peter L. Montgomery: "Division by Invariant
+  Integers using Multiplication". PLDI 1994.
+- Henry S. Warren, Jr: "Hacker's Delight". Addison-Wesley.  Chapter 10.
+*)
+
+Fixpoint find_div_mul_params (fuel: nat) (nc: Z) (d: Z) (p: Z) : option (Z * Z) :=
+  match fuel with
+  | O => None
+  | S fuel' =>
+      let twp := two_p p in
+      if zlt (nc * (d - twp mod d)) twp
+      then Some(p - 32, (twp + d - twp mod d) / d)
+      else find_div_mul_params fuel' nc d (p + 1)
+  end.
+
+Definition divs_mul_params (d: Z) : option (Z * Z) :=
+  match find_div_mul_params
+          Int.wordsize
+          (Int.half_modulus - Int.half_modulus mod d - 1)
+          d 32 with
+  | None => None
+  | Some(p, m) =>
+      if zlt 0 d
+      && zlt (two_p (32 + p)) (m * d)
+      && zle (m * d) (two_p (32 + p) + two_p (p + 1))
+      && zle 0 m && zlt m Int.modulus
+      && zle 0 p && zlt p 32
+      then Some(p, m) else None
+  end.
+
+Definition divu_mul_params (d: Z) : option (Z * Z) :=
+  match find_div_mul_params
+          Int.wordsize
+          (Int.modulus - Int.modulus mod d - 1)
+          d 32 with
+  | None => None
+  | Some(p, m) =>
+      if zlt 0 d
+      && zle (two_p (32 + p)) (m * d)
+      && zle (m * d) (two_p (32 + p) + two_p p)
+      && zle 0 m && zlt m Int.modulus
+      && zle 0 p && zlt p 32
+      then Some(p, m) else None
+  end.
+
+Definition divu_mul (p: Z) (m: Z) :=
+  shruimm (Eop Omulhu (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil))
+          (Int.repr p).
+
+Definition divuimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l => shruimm e1 l
+  | None =>
+      match divu_mul_params (Int.unsigned n2) with
+      | None => divu_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (divu_mul p m)
+      end
+  end.
+
+Nondetfunction divu (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => divuimm e1 n2
+  | _ => divu_base e1 e2
+  end.
+
+Definition mod_from_div (equo: expr) (n: int) :=
+  Eop Osub (Eletvar O ::: mulimm n equo ::: Enil).
+
+Definition moduimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l => andimm (Int.sub n2 Int.one) e1
+  | None =>
+      match divu_mul_params (Int.unsigned n2) with
+      | None => modu_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2)
+      end
+  end.
+
+Nondetfunction modu (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => moduimm e1 n2
+  | _ => modu_base e1 e2
+  end.
+
+Definition divs_mul (p: Z) (m: Z) :=
+  let e2 :=
+    Eop Omulhs (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil) in
+  let e3 :=
+    if zlt m Int.half_modulus then e2 else add e2 (Eletvar O) in
+  add (shrimm e3 (Int.repr p))
+      (shruimm (Eletvar O) (Int.repr (Int.zwordsize - 1))).
+
+Definition divsimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l => 
+      if Int.ltu l (Int.repr 31)
+      then shrximm e1 l
+      else divs_base e1 (Eop (Ointconst n2) Enil)
+  | None =>
+      match divs_mul_params (Int.signed n2) with
+      | None => divs_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (divs_mul p m)
+      end
+  end.
+
+Nondetfunction divs (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => divsimm e1 n2
+  | _ => divs_base e1 e2
+  end.
+
+Definition modsimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l =>
+      if Int.ltu l (Int.repr 31)
+      then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2)
+      else mods_base e1 (Eop (Ointconst n2) Enil)
+  | None =>
+      match divs_mul_params (Int.signed n2) with
+      | None => mods_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2)
+      end
+  end.
+
+Nondetfunction mods (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => modsimm e1 n2
+  | _ => mods_base e1 e2
+  end.
+
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
new file mode 100644
index 0000000..4d8f96a
--- /dev/null
+++ b/backend/SelectDivproof.v
@@ -0,0 +1,547 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness of instruction selection for integer division *)
+
+Require Import Coqlib.
+Require Import Zquot.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Cminor.
+Require Import Op.
+Require Import CminorSel.
+Require Import SelectOp.
+Require Import SelectOpproof.
+Require Import SelectDiv.
+
+Open Local Scope cminorsel_scope.
+
+(** * Main approximation theorems *)
+
+Section Z_DIV_MUL.
+
+Variable N: Z.      (**r number of relevant bits *)
+Hypothesis N_pos: N >= 0.
+Variable d: Z.      (**r divisor *)
+Hypothesis d_pos: d > 0.
+
+(** This is theorem 4.2 from Granlund and Montgomery, PLDI 1994. *)
+
+Lemma Zdiv_mul_pos:
+  forall m l,
+  l >= 0 ->
+  two_p (N+l) <= m * d <= two_p (N+l) + two_p l ->
+  forall n,
+  0 <= n < two_p N ->
+  Zdiv n d = Zdiv (m * n) (two_p (N + l)).
+Proof.
+  intros m l l_pos [LO HI] n RANGE.
+  exploit (Z_div_mod_eq n d). auto. 
+  set (q := n / d).
+  set (r := n mod d).
+  intro EUCL.
+  assert (0 <= r <= d - 1).
+    unfold r. generalize (Z_mod_lt n d d_pos). omega.
+  assert (0 <= m). 
+    apply Zmult_le_0_reg_r with d. auto.
+    exploit (two_p_gt_ZERO (N + l)). omega. omega. 
+  set (k := m * d - two_p (N + l)).
+  assert (0 <= k <= two_p l). 
+    unfold k; omega.
+  assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r).
+    unfold k. rewrite EUCL. ring.
+  assert (0 <= k * n).
+    apply Zmult_le_0_compat; omega.
+  assert (k * n <= two_p (N + l) - two_p l).
+    apply Zle_trans with (two_p l * n).
+    apply Zmult_le_compat_r. omega. omega.
+    replace (N + l) with (l + N) by omega.
+    rewrite two_p_is_exp. 
+    replace (two_p l * two_p N - two_p l)
+       with (two_p l * (two_p N - 1))
+         by ring.
+    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    omega. omega.
+  assert (0 <= two_p (N + l) * r).
+    apply Zmult_le_0_compat. 
+    exploit (two_p_gt_ZERO (N + l)). omega. omega.
+    omega.
+  assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
+    replace (two_p (N + l) * d - two_p (N + l))
+       with (two_p (N + l) * (d - 1)) by ring.
+    apply Zmult_le_compat_l.
+    omega.
+    exploit (two_p_gt_ZERO (N + l)). omega. omega.
+  assert (0 <= m * n - two_p (N + l) * q).
+    apply Zmult_le_reg_r with d. auto. 
+    replace (0 * d) with 0 by ring.  rewrite H2. omega. 
+  assert (m * n - two_p (N + l) * q < two_p (N + l)).
+    apply Zmult_lt_reg_r with d. omega.
+    rewrite H2. 
+    apply Zle_lt_trans with (two_p (N + l) * d - two_p l).
+    omega. 
+    exploit (two_p_gt_ZERO l). omega. omega.
+  symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). 
+  ring. omega.
+Qed.
+
+Lemma Zdiv_unique_2:
+  forall x y q, y > 0 -> 0 < y * q - x <= y -> Zdiv x y = q - 1.
+Proof.
+  intros. apply Zdiv_unique with (x - (q - 1) * y). ring. 
+  replace ((q - 1) * y) with (y * q - y) by ring. omega. 
+Qed.
+
+Lemma Zdiv_mul_opp:
+  forall m l,
+  l >= 0 ->
+  two_p (N+l) < m * d <= two_p (N+l) + two_p l ->
+  forall n,
+  0 < n <= two_p N ->
+  Zdiv n d = - Zdiv (m * (-n)) (two_p (N + l)) - 1.
+Proof.
+  intros m l l_pos [LO HI] n RANGE.
+  replace (m * (-n)) with (- (m * n)) by ring.
+  exploit (Z_div_mod_eq n d). auto. 
+  set (q := n / d).
+  set (r := n mod d).
+  intro EUCL.
+  assert (0 <= r <= d - 1).
+    unfold r. generalize (Z_mod_lt n d d_pos). omega.
+  assert (0 <= m). 
+    apply Zmult_le_0_reg_r with d. auto.
+    exploit (two_p_gt_ZERO (N + l)). omega. omega.
+  cut (Zdiv (- (m * n)) (two_p (N + l)) = -q - 1).
+    omega.
+  apply Zdiv_unique_2. 
+  apply two_p_gt_ZERO. omega.
+  replace (two_p (N + l) * - q - - (m * n))
+     with (m * n - two_p (N + l) * q)
+       by ring.
+  set (k := m * d - two_p (N + l)).
+  assert (0 < k <= two_p l). 
+    unfold k; omega.
+  assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r).
+    unfold k. rewrite EUCL. ring.
+  split.
+  apply Zmult_lt_reg_r with d. omega. 
+  replace (0 * d) with 0 by omega.
+  rewrite H2.
+  assert (0 < k * n). apply Zmult_lt_0_compat; omega.
+  assert (0 <= two_p (N + l) * r).
+    apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)); omega. omega.
+  omega.
+  apply Zmult_le_reg_r with d. omega.
+  rewrite H2. 
+  assert (k * n <= two_p (N + l)).
+    rewrite Zplus_comm. rewrite two_p_is_exp; try omega. 
+    apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. 
+    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+  assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
+    replace (two_p (N + l) * d - two_p (N + l))
+       with (two_p (N + l) * (d - 1))
+         by ring.
+    apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO (N + l)). omega. omega.
+  omega.
+Qed.
+
+(** This is theorem 5.1 from Granlund and Montgomery, PLDI 1994. *)
+
+Lemma Zquot_mul:
+  forall m l,
+  l >= 0 ->
+  two_p (N+l) < m * d <= two_p (N+l) + two_p l ->
+  forall n,
+  - two_p N <= n < two_p N ->
+  Z.quot n d = Zdiv (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0).
+Proof.
+  intros. destruct (zlt n 0).
+  exploit (Zdiv_mul_opp m l H H0 (-n)). omega. 
+  replace (- - n) with n by ring.
+  replace (Z.quot n d) with (- Z.quot (-n) d).
+  rewrite Zquot_Zdiv_pos by omega. omega.
+  rewrite Z.quot_opp_l by omega. ring.
+  rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega. 
+  apply Zdiv_mul_pos; omega.
+Qed.
+
+End Z_DIV_MUL.
+
+(** * Correctness of the division parameters *)
+
+Lemma divs_mul_params_sound:
+  forall d m p,
+  divs_mul_params d = Some(p, m) ->
+  0 <= m < Int.modulus /\ 0 <= p < 32 /\
+  forall n,
+  Int.min_signed <= n <= Int.max_signed ->
+  Z.quot n d = Zdiv (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0).
+Proof with (try discriminate).
+  unfold divs_mul_params; intros d m' p' EQ.
+  destruct (find_div_mul_params Int.wordsize
+               (Int.half_modulus - Int.half_modulus mod d - 1) d 32)
+  as [[p m] | ]...
+  destruct (zlt 0 d)...
+  destruct (zlt (two_p (32 + p)) (m * d))...
+  destruct (zle (m * d) (two_p (32 + p) + two_p (p + 1)))...
+  destruct (zle 0 m)...
+  destruct (zlt m Int.modulus)...
+  destruct (zle 0 p)...
+  destruct (zlt p 32)...
+  simpl in EQ. inv EQ. 
+  split. auto. split. auto. intros. 
+  replace (32 + p') with (31 + (p' + 1)) by omega. 
+  apply Zquot_mul; try omega.
+  replace (31 + (p' + 1)) with (32 + p') by omega. omega.
+  change (Int.min_signed <= n < Int.half_modulus). 
+  unfold Int.max_signed in H. omega. 
+Qed.
+
+Lemma divu_mul_params_sound:
+  forall d m p,
+  divu_mul_params d = Some(p, m) ->
+  0 <= m < Int.modulus /\ 0 <= p < 32 /\
+  forall n,
+  0 <= n < Int.modulus ->
+  Zdiv n d = Zdiv (m * n) (two_p (32 + p)).
+Proof with (try discriminate).
+  unfold divu_mul_params; intros d m' p' EQ.
+  destruct (find_div_mul_params Int.wordsize
+               (Int.modulus - Int.modulus mod d - 1) d 32)
+  as [[p m] | ]...
+  destruct (zlt 0 d)...
+  destruct (zle (two_p (32 + p)) (m * d))...
+  destruct (zle (m * d) (two_p (32 + p) + two_p p))...
+  destruct (zle 0 m)...
+  destruct (zlt m Int.modulus)...
+  destruct (zle 0 p)...
+  destruct (zlt p 32)...
+  simpl in EQ. inv EQ. 
+  split. auto. split. auto. intros.
+  apply Zdiv_mul_pos; try omega. assumption.
+Qed.
+
+Lemma divs_mul_shift_gen:
+  forall x y m p,
+  divs_mul_params (Int.signed y) = Some(p, m) ->
+  0 <= m < Int.modulus /\ 0 <= p < 32 /\
+  Int.divs x y = Int.add (Int.shr (Int.repr ((Int.signed x * m) / Int.modulus)) (Int.repr p))
+                         (Int.shru x (Int.repr 31)).
+Proof.
+  intros. set (n := Int.signed x). set (d := Int.signed y) in *.
+  exploit divs_mul_params_sound; eauto. intros (A & B & C).
+  split. auto. split. auto.
+  unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range). 
+  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. 
+  rewrite Int.shru_lt_zero. unfold Int.add. apply Int.eqm_samerepr. apply Int.eqm_add.
+  rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2. 
+  rewrite Int.unsigned_repr. f_equal.
+  rewrite Int.signed_repr. rewrite Int.modulus_power. f_equal. ring.
+  cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus). 
+  unfold Int.max_signed; omega. 
+  apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. 
+  apply Int.modulus_pos.
+  split. apply Zle_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega.
+  apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto.
+  apply Zle_lt_trans with (Int.half_modulus * m). 
+  apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto.
+  apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. 
+  assert (32 < Int.max_unsigned) by (compute; auto). omega.
+  unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr. 
+  apply two_p_gt_ZERO. omega.
+  apply two_p_gt_ZERO. omega.
+Qed.
+
+Theorem divs_mul_shift_1:
+  forall x y m p,
+  divs_mul_params (Int.signed y) = Some(p, m) ->
+  m < Int.half_modulus ->
+  0 <= p < 32 /\
+  Int.divs x y = Int.add (Int.shr (Int.mulhs x (Int.repr m)) (Int.repr p))
+                         (Int.shru x (Int.repr 31)).
+Proof.
+  intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). 
+  intros (A & B & C). split. auto. rewrite C. 
+  unfold Int.mulhs. rewrite Int.signed_repr. auto.
+  generalize Int.min_signed_neg; unfold Int.max_signed; omega.
+Qed.
+
+Theorem divs_mul_shift_2:
+  forall x y m p,
+  divs_mul_params (Int.signed y) = Some(p, m) ->
+  m >= Int.half_modulus ->
+  0 <= p < 32 /\
+  Int.divs x y = Int.add (Int.shr (Int.add (Int.mulhs x (Int.repr m)) x) (Int.repr p))
+                         (Int.shru x (Int.repr 31)).
+Proof.
+  intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). 
+  intros (A & B & C). split. auto. rewrite C. f_equal. f_equal.
+  rewrite Int.add_signed. unfold Int.mulhs. set (n := Int.signed x).
+  transitivity (Int.repr (n * (m - Int.modulus) / Int.modulus + n)).
+  f_equal. 
+  replace (n * (m - Int.modulus)) with (n * m +  (-n) * Int.modulus) by ring.
+  rewrite Z_div_plus. ring. apply Int.modulus_pos. 
+  apply Int.eqm_samerepr. apply Int.eqm_add; auto with ints. 
+  apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned. 
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. f_equal. f_equal. 
+  rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption. 
+  apply zlt_false. omega.
+Qed.
+
+Theorem divu_mul_shift:
+  forall x y m p,
+  divu_mul_params (Int.unsigned y) = Some(p, m) ->
+  0 <= p < 32 /\
+  Int.divu x y = Int.shru (Int.mulhu x (Int.repr m)) (Int.repr p).
+Proof.
+  intros. exploit divu_mul_params_sound; eauto. intros (A & B & C).
+  split. auto. 
+  rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr. 
+  unfold Int.divu, Int.mulhu. f_equal. rewrite C by apply Int.unsigned_range.
+  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega).
+  f_equal. rewrite (Int.unsigned_repr m). 
+  rewrite Int.unsigned_repr. f_equal. ring.
+  cut (0 <= Int.unsigned x * m / Int.modulus < Int.modulus).
+  unfold Int.max_unsigned; omega.
+  apply Zdiv_interval_1. omega. compute; auto. compute; auto.
+  split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. 
+  apply Zle_lt_trans with (Int.modulus * m).
+  apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. 
+  apply Zmult_lt_compat_l. compute; auto. omega. 
+  unfold Int.max_unsigned; omega.
+  assert (32 < Int.max_unsigned) by (compute; auto). omega.
+Qed.
+
+(** * Correctness of the smart constructors for division and modulus *)
+
+Section CMCONSTRS.
+
+Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
+Lemma eval_divu_mul:
+  forall le x y p M,
+  divu_mul_params (Int.unsigned y) = Some(p, M) ->
+  nth_error le O = Some (Vint x) ->
+  eval_expr ge sp e m le (divu_mul p M) (Vint (Int.divu x y)).
+Proof.
+  intros. unfold divu_mul. exploit (divu_mul_shift x); eauto. intros [A B].
+  assert (eval_expr ge sp e m le
+           (Eop Omulhu (Eletvar 0 ::: Eop (Ointconst (Int.repr M)) Enil ::: Enil))
+           (Vint (Int.mulhu x (Int.repr M)))).
+  { EvalOp. econstructor. econstructor; eauto. econstructor. EvalOp. simpl; reflexivity. constructor.
+    auto. }
+  exploit eval_shruimm. eexact H1. instantiate (1 := Int.repr p). 
+  intros [v [P Q]]. simpl in Q. 
+  replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q. 
+  inv Q. rewrite B. auto. 
+  unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto.
+  assert (32 < Int.max_unsigned) by (compute; auto). omega.
+Qed.
+
+Theorem eval_divuimm:
+  forall le e1 x n2 z,
+  eval_expr ge sp e m le e1 x ->
+  Val.divu x (Vint n2) = Some z ->
+  exists v, eval_expr ge sp e m le (divuimm e1 n2) v /\ Val.lessdef z v.
+Proof.
+  unfold divuimm; intros. generalize H0; intros DIV.
+  destruct x; simpl in DIV; try discriminate.
+  destruct (Int.eq n2 Int.zero) eqn:Z2; inv DIV. 
+  destruct (Int.is_power2 n2) as [l | ] eqn:P2.
+- erewrite Int.divu_pow2 by eauto. 
+  replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). 
+  apply eval_shruimm; auto.
+  simpl. erewrite Int.is_power2_range; eauto. 
+- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+  + exists (Vint (Int.divu i n2)); split; auto.
+    econstructor; eauto. eapply eval_divu_mul; eauto. 
+  + eapply eval_divu_base; eauto. EvalOp.
+Qed.
+
+Theorem eval_divu:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.divu x y = Some z ->
+  exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v.
+Proof.
+  unfold divu; intros until b. destruct (divu_match b); intros.
+- inv H0. inv H5. simpl in H7. inv H7. eapply eval_divuimm; eauto.
+- eapply eval_divu_base; eauto. 
+Qed.
+
+Lemma eval_mod_from_div:
+  forall le a n x y,
+  eval_expr ge sp e m le a (Vint y) ->
+  nth_error le O = Some (Vint x) ->
+  eval_expr ge sp e m le (mod_from_div a n) (Vint (Int.sub x (Int.mul y n))).
+Proof.
+  unfold mod_from_div; intros. 
+  exploit eval_mulimm; eauto. instantiate (1 := n). intros [v [A B]]. 
+  simpl in B. inv B. EvalOp.
+Qed.
+
+Theorem eval_moduimm:
+  forall le e1 x n2 z,
+  eval_expr ge sp e m le e1 x ->
+  Val.modu x (Vint n2) = Some z ->
+  exists v, eval_expr ge sp e m le (moduimm e1 n2) v /\ Val.lessdef z v.
+Proof.
+  unfold moduimm; intros. generalize H0; intros MOD.
+  destruct x; simpl in MOD; try discriminate.
+  destruct (Int.eq n2 Int.zero) eqn:Z2; inv MOD. 
+  destruct (Int.is_power2 n2) as [l | ] eqn:P2.
+- erewrite Int.modu_and by eauto.
+  change (Vint (Int.and i (Int.sub n2 Int.one)))
+    with (Val.and (Vint i) (Vint (Int.sub n2 Int.one))).
+  apply eval_andimm. auto.
+- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+  + econstructor; split. 
+    econstructor; eauto. eapply eval_mod_from_div. 
+    eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. 
+    rewrite Int.modu_divu. auto. 
+    red; intros; subst n2; discriminate.
+  + eapply eval_modu_base; eauto. EvalOp.
+Qed.
+
+Theorem eval_modu:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.modu x y = Some z ->
+  exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
+Proof.
+  unfold modu; intros until b. destruct (modu_match b); intros.
+- inv H0. inv H5. simpl in H7. inv H7. eapply eval_moduimm; eauto.
+- eapply eval_modu_base; eauto. 
+Qed.
+
+Lemma eval_divs_mul:
+  forall le x y p M,
+  divs_mul_params (Int.signed y) = Some(p, M) ->
+  nth_error le O = Some (Vint x) ->
+  eval_expr ge sp e m le (divs_mul p M) (Vint (Int.divs x y)).
+Proof.
+  intros. unfold divs_mul.
+  assert (V: eval_expr ge sp e m le (Eletvar O) (Vint x)).
+  { constructor; auto. }
+  assert (X: eval_expr ge sp e m le
+           (Eop Omulhs (Eletvar 0 ::: Eop (Ointconst (Int.repr M)) Enil ::: Enil))
+           (Vint (Int.mulhs x (Int.repr M)))).
+  { EvalOp. econstructor. eauto. econstructor. EvalOp. simpl; reflexivity. constructor.
+    auto. }
+  exploit eval_shruimm. eexact V. instantiate (1 := Int.repr (Int.zwordsize - 1)). 
+  intros [v1 [Y LD]]. simpl in LD. 
+  change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. 
+  simpl in LD. inv LD. 
+  assert (RANGE: 0 <= p < 32 -> Int.ltu (Int.repr p) Int.iwordsize = true).
+  { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto.
+    assert (32 < Int.max_unsigned) by (compute; auto). omega. }
+  destruct (zlt M Int.half_modulus).
+- exploit (divs_mul_shift_1 x); eauto. intros [A B].
+  exploit eval_shrimm. eexact X. instantiate (1 := Int.repr p). intros [v1 [Z LD]].
+  simpl in LD. rewrite RANGE in LD by auto. inv LD.
+  exploit eval_add. eexact Z. eexact Y. intros [v1 [W LD]].
+  simpl in LD. inv LD. 
+  rewrite B. exact W.
+- exploit (divs_mul_shift_2 x); eauto. intros [A B].
+  exploit eval_add. eexact X. eexact V. intros [v1 [Z LD]]. 
+  simpl in LD. inv LD. 
+  exploit eval_shrimm. eexact Z. instantiate (1 := Int.repr p). intros [v1 [U LD]].
+  simpl in LD. rewrite RANGE in LD by auto. inv LD.
+  exploit eval_add. eexact U. eexact Y. intros [v1 [W LD]].
+  simpl in LD. inv LD. 
+  rewrite B. exact W.
+Qed.
+
+Theorem eval_divsimm:
+  forall le e1 x n2 z,
+  eval_expr ge sp e m le e1 x ->
+  Val.divs x (Vint n2) = Some z ->
+  exists v, eval_expr ge sp e m le (divsimm e1 n2) v /\ Val.lessdef z v.
+Proof.
+  unfold divsimm; intros. generalize H0; intros DIV.
+  destruct x; simpl in DIV; try discriminate.
+  destruct (Int.eq n2 Int.zero
+            || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. 
+  destruct (Int.is_power2 n2) as [l | ] eqn:P2.
+- destruct (Int.ltu l (Int.repr 31)) eqn:LT31.
+  + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto.
+  + eapply eval_divs_base; eauto. EvalOp.
+- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
+  + exists (Vint (Int.divs i n2)); split; auto.
+    econstructor; eauto. eapply eval_divs_mul; eauto. 
+  + eapply eval_divs_base; eauto. EvalOp.
+Qed.
+
+Theorem eval_divs:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.divs x y = Some z ->
+  exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v.
+Proof.
+  unfold divs; intros until b. destruct (divs_match b); intros.
+- inv H0. inv H5. simpl in H7. inv H7. eapply eval_divsimm; eauto.
+- eapply eval_divs_base; eauto. 
+Qed.
+
+Theorem eval_modsimm:
+  forall le e1 x n2 z,
+  eval_expr ge sp e m le e1 x ->
+  Val.mods x (Vint n2) = Some z ->
+  exists v, eval_expr ge sp e m le (modsimm e1 n2) v /\ Val.lessdef z v.
+Proof.
+  unfold modsimm; intros. 
+  exploit Val.mods_divs; eauto. intros [y [A B]].
+  generalize A; intros DIV.
+  destruct x; simpl in DIV; try discriminate.
+  destruct (Int.eq n2 Int.zero
+            || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. 
+  destruct (Int.is_power2 n2) as [l | ] eqn:P2.
+- destruct (Int.ltu l (Int.repr 31)) eqn:LT31.
+  + exploit (eval_shrximm ge sp e m (Vint i :: le) (Eletvar O)).
+    constructor. simpl; eauto. eapply Val.divs_pow2; eauto. 
+    intros [v1 [X LD]]. inv LD. 
+    econstructor; split. econstructor. eauto. 
+    apply eval_mod_from_div. eexact X. simpl; eauto. 
+    simpl. auto.
+  + eapply eval_mods_base; eauto. EvalOp.
+- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
+  + econstructor; split. 
+    econstructor. eauto. apply eval_mod_from_div with (x := i); auto.
+    eapply eval_divs_mul with (x := i); eauto.
+    simpl. auto.
+  + eapply eval_mods_base; eauto. EvalOp.
+Qed.
+
+Theorem eval_mods:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.mods x y = Some z ->
+  exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v.
+Proof.
+  unfold mods; intros until b. destruct (mods_match b); intros.
+- inv H0. inv H5. simpl in H7. inv H7. eapply eval_modsimm; eauto.
+- eapply eval_mods_base; eauto. 
+Qed.
+
+End CMCONSTRS.
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index 3978828..26f33da 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Correctness of instruction selection for 64-bit integer operations *)
+(** Correctness of instruction selection for integer division *)
 
 Require Import Coqlib.
 Require Import AST.
diff --git a/backend/Selection.v b/backend/Selection.v
index b35c891..f62a888 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -31,6 +31,7 @@ Require Cminor.
 Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
+Require Import SelectDiv.
 Require Import SelectLong.
 
 Open Local Scope cminorsel_scope.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index e94f85d..c292b49 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -26,9 +26,11 @@ Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
+Require Import SelectDiv.
 Require Import SelectLong.
 Require Import Selection.
 Require Import SelectOpproof.
+Require Import SelectDivproof.
 Require Import SelectLongproof.
 
 Open Local Scope cminorsel_scope.
diff --git a/common/Values.v b/common/Values.v
index 05749b7..670f785 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -222,6 +222,18 @@ Definition mul (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
+Definition mulhs (v1 v2: val): val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Vint(Int.mulhs n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition mulhu (v1 v2: val): val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Vint(Int.mulhu n1 n2)
+  | _, _ => Vundef
+  end.
+
 Definition divs (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
diff --git a/ia32/Asm.v b/ia32/Asm.v
index d86ff19..78c4c3b 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -145,6 +145,8 @@ Inductive instruction: Type :=
   | Psub_rr (rd: ireg) (r1: ireg)
   | Pimul_rr (rd: ireg) (r1: ireg)
   | Pimul_ri (rd: ireg) (n: int)
+  | Pimul_r (r1: ireg)
+  | Pmul_r (r1: ireg)
   | Pdiv (r1: ireg)
   | Pidiv (r1: ireg)
   | Pand_rr (rd: ireg) (r1: ireg)
@@ -540,6 +542,12 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd rs#r1))) m
   | Pimul_ri rd n =>
       Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd (Vint n)))) m
+  | Pimul_r r1 =>
+      Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1)
+                            #EDX <- (Val.mulhs rs#EAX rs#r1))) m
+  | Pmul_r r1 =>
+      Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1)
+                            #EDX <- (Val.mulhu rs#EAX rs#r1))) m
   | Pdiv r1 =>
       let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in
       match Val.divu vn vd, Val.modu vn vd with
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 4543ac9..0410057 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -311,6 +311,14 @@ Definition transl_op
   | Omulimm n, a1 :: nil =>
       assertion (mreg_eq a1 res);
       do r <- ireg_of res; OK (Pimul_ri r n :: k)
+  | Omulhs, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 AX);
+      assertion (mreg_eq res DX);
+      do r2 <- ireg_of a2; OK (Pimul_r r2 :: k)
+  | Omulhu, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 AX);
+      assertion (mreg_eq res DX);
+      do r2 <- ireg_of a2; OK (Pmul_r r2 :: k)
   | Odiv, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 AX);
       assertion (mreg_eq a2 CX);
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 728617e..9ddc463 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -922,6 +922,10 @@ Transparent destroyed_by_op.
   apply SAME. eapply mk_intconv_correct; eauto.
 (* cast16unsigned *)
   apply SAME. eapply mk_intconv_correct; eauto.
+(* mulhs *)
+  apply SAME. TranslOp. destruct H1. Simplifs. 
+(* mulhu *)
+  apply SAME. TranslOp. destruct H1. Simplifs. 
 (* div *)
   apply SAME.
   specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. 
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index fea0afd..a29b450 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -107,6 +107,8 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
   | Omulimm n, I n1 :: nil => I(Int.mul n1 n)
+  | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2)
+  | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu n1 n2)
   | Odiv, I n1 :: I n2 :: nil =>
       if Int.eq n2 Int.zero then Unknown else
       if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 528e9ed..826dadf 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -75,6 +75,8 @@ Definition destroyed_by_op (op: operation): list mreg :=
   match op with
   | Omove => FP0 :: nil
   | Ocast8signed | Ocast8unsigned | Ocast16signed | Ocast16unsigned => AX :: nil
+  | Omulhs => AX :: DX :: nil
+  | Omulhu => AX :: DX :: nil
   | Odiv => AX :: DX :: nil
   | Odivu => AX :: DX :: nil
   | Omod => AX :: DX :: nil
@@ -136,6 +138,8 @@ Definition temp_for_parent_frame: mreg :=
 
 Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
   match op with
+  | Omulhs => (Some AX :: None :: nil, Some DX)
+  | Omulhu => (Some AX :: None :: nil, Some DX)
   | Odiv => (Some AX :: Some CX :: nil, Some AX)
   | Odivu => (Some AX :: Some CX :: nil, Some AX)
   | Omod => (Some AX :: Some CX :: nil, Some DX)
@@ -192,6 +196,8 @@ Definition two_address_op (op: operation) : bool :=
   | Osub => true
   | Omul => true
   | Omulimm _ => true
+  | Omulhs => false
+  | Omulhu => false
   | Odiv => false
   | Odivu => false
   | Omod => false
diff --git a/ia32/Op.v b/ia32/Op.v
index 509938e..f2e6b13 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -78,6 +78,8 @@ Inductive operation : Type :=
   | Osub: operation                     (**r [rd = r1 - r2] *)
   | Omul: operation                     (**r [rd = r1 * r2] *)
   | Omulimm: int -> operation           (**r [rd = r1 * n] *)
+  | Omulhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omulhu: operation                   (**r [rd = high part of r1 * r2, unsigned] *)
   | Odiv: operation                     (**r [rd = r1 / r2] (signed) *)
   | Odivu: operation                    (**r [rd = r1 / r2] (unsigned) *)
   | Omod: operation                     (**r [rd = r1 % r2] (signed) *)
@@ -216,6 +218,8 @@ Definition eval_operation
   | Osub, v1::v2::nil => Some (Val.sub v1 v2)
   | Omul, v1::v2::nil => Some (Val.mul v1 v2)
   | Omulimm n, v1::nil => Some (Val.mul v1 (Vint n))
+  | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
+  | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
   | Odiv, v1::v2::nil => Val.divs v1 v2
   | Odivu, v1::v2::nil => Val.divu v1 v2
   | Omod, v1::v2::nil => Val.mods v1 v2
@@ -305,6 +309,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osub => (Tint :: Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
   | Omulimm _ => (Tint :: nil, Tint)
+  | Omulhs => (Tint :: Tint :: nil, Tint)
+  | Omulhu => (Tint :: Tint :: nil, Tint)
   | Odiv => (Tint :: Tint :: nil, Tint)
   | Odivu => (Tint :: Tint :: nil, Tint)
   | Omod => (Tint :: Tint :: nil, Tint)
@@ -387,6 +393,8 @@ Proof with (try exact I).
   destruct v0; destruct v1... simpl. destruct (eq_block b b0)...
   destruct v0; destruct v1...
   destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
   destruct v0; destruct v1; simpl in *; inv H0.
     destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
   destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
@@ -796,6 +804,8 @@ Proof.
     rewrite Int.sub_shifted. 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 (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 9c8f963..5fb2568 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -606,6 +606,10 @@ let print_instruction oc = function
       fprintf oc "	imull	%a, %a\n" ireg r1 ireg rd
   | Pimul_ri(rd, n) ->
       fprintf oc "	imull	$%a, %a\n" coqint n ireg rd
+  | Pimul_r(r1) ->
+      fprintf oc "	imull	%a\n" ireg r1
+  | Pmul_r(r1) ->
+      fprintf oc "	mull	%a\n" ireg r1
   | Pdiv(r1) ->
       fprintf oc "	xorl	%%edx, %%edx\n";
       fprintf oc "	divl	%a\n" ireg r1
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 2d1ab48..209147e 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -299,10 +299,13 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divu (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
-Definition modu (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-Definition mods (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
+
+Definition shrximm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
 
 (** ** General shifts *)
 
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 8c9c7e6..85802b6 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -471,44 +471,61 @@ Proof.
   TrivialExists.
 Qed.
 
-Theorem eval_divs:
+Theorem eval_divs_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divs x y = Some z ->
-  exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divs. exists z; split. EvalOp. auto.
+  intros. unfold divs_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_divu:
+Theorem eval_divu_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divu x y = Some z ->
-  exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divu. exists z; split. EvalOp. auto.
+  intros. unfold divu_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_mods:
+Theorem eval_mods_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.mods x y = Some z ->
-  exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold mods. exists z; split. EvalOp. auto.
+  intros. unfold mods_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_modu:
+Theorem eval_modu_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.modu x y = Some z ->
-  exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold modu. exists z; split. EvalOp. auto.
+  intros. unfold modu_base. exists z; split. EvalOp. auto.
+Qed.
+
+Theorem eval_shrximm:
+  forall le a n x z,
+  eval_expr ge sp e m le a x ->
+  Val.shrx x (Vint n) = Some z ->
+  exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
+Proof.
+  intros. unfold shrximm. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  subst n. exists x; split; auto. 
+  destruct x; simpl in H0; try discriminate.
+  destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
+  replace (Int.shrx i Int.zero) with i. auto. 
+  unfold Int.shrx, Int.divs. rewrite Int.shl_zero. 
+  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+  econstructor; split. EvalOp. auto.
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
diff --git a/lib/Integers.v b/lib/Integers.v
index 23f2294..cbbf28c 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -286,6 +286,11 @@ Definition rolm (x a m: int): int := and (rol x a) m.
 Definition shrx (x y: int): int :=
   divs x (shl one y).
 
+(** High half of full multiply. *)
+
+Definition mulhu (x y: int): int := repr ((unsigned x * unsigned y) / modulus).
+Definition mulhs (x y: int): int := repr ((signed x * signed y) / modulus).
+
 (** Condition flags *)
 
 Definition negative (x: int): int :=
@@ -4275,6 +4280,19 @@ Qed.
 
 Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y).
 
+Lemma mul'_mulhu:
+  forall x y, mul' x y = ofwords (Int.mulhu x y) (Int.mul x y).
+Proof.
+  intros. 
+  rewrite ofwords_add. unfold mul', Int.mulhu, Int.mul. 
+  set (p := Int.unsigned x * Int.unsigned y).
+  set (ph := p / Int.modulus). set (pl := p mod Int.modulus). 
+  transitivity (repr (ph * Int.modulus + pl)).
+- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos. 
+- apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. auto with ints.
+  rewrite Int.unsigned_repr_eq. apply eqm_refl.
+Qed.
+
 Lemma decompose_mul:
   forall xh xl yh yl,
   mul (ofwords xh xl) (ofwords yh yl) =
@@ -4310,6 +4328,16 @@ Proof.
   f_equal. ring. 
 Qed.
 
+Lemma decompose_mul_2:
+  forall xh xl yh yl,
+  mul (ofwords xh xl) (ofwords yh yl) =
+  ofwords (Int.add (Int.add (Int.mulhu xl yl) (Int.mul xl yh)) (Int.mul xh yl))
+          (Int.mul xl yl).
+Proof.
+  intros. rewrite decompose_mul. rewrite mul'_mulhu. 
+  rewrite hi_ofwords, lo_ofwords. auto.
+Qed.
+
 Lemma decompose_ltu:
   forall xh xl yh yl,
   ltu (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.ltu xh yh.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index bbe2d3e..e6e9d76 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -193,6 +193,8 @@ Inductive instruction : Type :=
   | Pmtlr: ireg -> instruction                                (**r move ireg to LR *)
   | Pmulli: ireg -> ireg -> constant -> instruction           (**r integer multiply immediate *)
   | Pmullw: ireg -> ireg -> ireg -> instruction               (**r integer multiply *)
+  | Pmulhw: ireg -> ireg -> ireg -> instruction               (**r multiply high signed *)
+  | Pmulhwu: ireg -> ireg -> ireg -> instruction               (**r multiply high signed *)
   | Pnand: ireg -> ireg -> ireg -> instruction                (**r bitwise not-and *)
   | Pnor: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-or *)
   | Por: ireg -> ireg -> ireg -> instruction                  (**r bitwise or *)
@@ -702,6 +704,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       Next (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m
   | Pmullw rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m
+  | Pmulhw rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.mulhs rs#r1 rs#r2))) m
+  | Pmulhwu rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.mulhu rs#r1 rs#r2))) m
   | Pnand rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m
   | Pnor rd r1 r2 =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 2b6d80d..cc9a51c 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -371,6 +371,12 @@ Definition transl_op
            Pmulli r r1 (Cint n) :: k
          else
            loadimm GPR0 n (Pmullw r r1 GPR0 :: k))
+  | Omulhs, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pmulhw r r1 r2 :: k)
+  | Omulhu, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pmulhwu r r1 r2 :: k)
   | Odiv, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
       OK (Pdivw r r1 r2 :: k)
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index e7e4095..d0322c1 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -95,6 +95,8 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osubimm n, I n1 :: nil => I (Int.sub n n1)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
   | Omulimm n, I n1 :: nil => I(Int.mul n1 n)
+  | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2)
+  | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu n1 n2)
   | Odiv, I n1 :: I n2 :: nil =>
       if Int.eq n2 Int.zero then Unknown else
       if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 1952304..085a098 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -65,6 +65,8 @@ Inductive operation : Type :=
   | Osubimm: int -> operation           (**r [rd = n - r1] *)
   | Omul: operation                     (**r [rd = r1 * r2] *)
   | Omulimm: int -> operation           (**r [rd = r1 * n] *)
+  | Omulhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omulhu: operation                   (**r [rd = high part of r1 * r2, unsigned] *)
   | Odiv: operation                     (**r [rd = r1 / r2] (signed) *)
   | Odivu: operation                    (**r [rd = r1 / r2] (unsigned) *)
   | Oand: operation                     (**r [rd = r1 & r2] *)
@@ -185,6 +187,8 @@ Definition eval_operation
   | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1)
   | Omul, v1::v2::nil => Some (Val.mul v1 v2)
   | Omulimm n, v1::nil => Some (Val.mul v1 (Vint n))
+  | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
+  | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
   | Odiv, v1::v2::nil => Val.divs v1 v2
   | Odivu, v1::v2::nil => Val.divu v1 v2
   | Oand, v1::v2::nil => Some(Val.and v1 v2)
@@ -276,6 +280,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubimm _ => (Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
   | Omulimm _ => (Tint :: nil, Tint)
+  | Omulhs => (Tint :: Tint :: nil, Tint)
+  | Omulhu => (Tint :: Tint :: nil, Tint)
   | Odiv => (Tint :: Tint :: nil, Tint)
   | Odivu => (Tint :: Tint :: nil, Tint)
   | Oand => (Tint :: Tint :: nil, Tint)
@@ -351,6 +357,8 @@ Proof with (try exact I).
   destruct v0...
   destruct v0; destruct v1...
   destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
   destruct v0; destruct v1; simpl in *; inv H0.
     destruct (Int.eq i0 Int.zero
          || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
@@ -759,6 +767,8 @@ Proof.
   inv H4; 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 (Int.eq i0 Int.zero
          || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 879d755..08438df 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -818,6 +818,10 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	mulli	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pmullw(r1, r2, r3) ->
       fprintf oc "	mullw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pmulhw(r1, r2, r3) ->
+      fprintf oc "	mulhw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pmulhwu(r1, r2, r3) ->
+      fprintf oc "	mulhwu	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pnand(r1, r2, r3) ->
       fprintf oc "	nand	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pnor(r1, r2, r3) ->
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 7b15ccc..bc9b677 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -290,8 +290,6 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-
 Definition mod_aux (divop: operation) (e1 e2: expr) :=
   Elet e1
     (Elet (lift e2)
@@ -301,31 +299,13 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
                            Enil) :::
                  Enil))).
 
-Definition mods := mod_aux Odiv.
-
-Definition divuimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => shruimm e l
-  | None   => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
-  end.
-
-Nondetfunction divu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => divuimm e1 n2
-  | _ => Eop Odivu (e1:::e2:::Enil)
-  end.
-
-Definition moduimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => andimm (Int.sub n Int.one) e
-  | None   => mod_aux Odivu e (Eop (Ointconst n) Enil)
-  end.
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base := mod_aux Odiv.
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base := mod_aux Odivu.
 
-Nondetfunction modu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => moduimm e1 n2
-  | _ => mod_aux Odivu e1 e2
-  end.
+Definition shrximm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
 
 (** ** General shifts *)
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 5a0a903..177d64a 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -465,14 +465,14 @@ Proof.
   TrivialExists.
 Qed.
 
-Theorem eval_divs:
+Theorem eval_divs_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divs x y = Some z ->
-  exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divs. exists z; split. EvalOp. auto.
+  intros. unfold divs_base. exists z; split. EvalOp. auto.
 Qed.
 
 Lemma eval_mod_aux:
@@ -501,73 +501,57 @@ Proof.
   reflexivity.
 Qed.
 
-Theorem eval_mods:
+Theorem eval_mods_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.mods x y = Some z ->
-  exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold mods. 
+  intros; unfold mods_base. 
   exploit Val.mods_divs; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divs); auto.
 Qed.
 
-Theorem eval_divuimm:
-  forall le n a x z,
-  eval_expr ge sp e m le a x ->
-  Val.divu x (Vint n) = Some z ->
-  exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v.
-Proof.
-  intros; unfold divuimm. 
-  destruct (Int.is_power2 n) eqn:?. 
-  replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto.
-  eapply Val.divu_pow2; eauto.
-  TrivialExists. 
-  econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
-Qed.
-
-Theorem eval_divu:
-  forall le a x b y z,
+Theorem eval_divu_base:
+  forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divu x y = Some z ->
-  exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros until z. unfold divu; destruct (divu_match b); intros; InvEval.
-  eapply eval_divuimm; eauto.
-  TrivialExists. 
+  intros. unfold divu_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_moduimm:
-  forall le n a x z,
+Theorem eval_modu_base:
+  forall le a b x y z,
   eval_expr ge sp e m le a x ->
-  Val.modu x (Vint n) = Some z ->
-  exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v.
+  eval_expr ge sp e m le b y ->
+  Val.modu x y = Some z ->
+  exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold moduimm. 
-  destruct (Int.is_power2 n) eqn:?. 
-  replace z with (Val.and x (Vint (Int.sub n Int.one))). apply eval_andimm; auto.
-  eapply Val.modu_pow2; eauto.
+  intros; unfold modu_base. 
   exploit Val.modu_divu; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divu); auto.
-  EvalOp.
 Qed.
 
-Theorem eval_modu:
-  forall le a x b y z,
+Theorem eval_shrximm:
+  forall le a n x z,
   eval_expr ge sp e m le a x ->
-  eval_expr ge sp e m le b y ->
-  Val.modu x y = Some z ->
-  exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
+  Val.shrx x (Vint n) = Some z ->
+  exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
 Proof.
-  intros until y; unfold modu; case (modu_match b); intros; InvEval.
-  eapply eval_moduimm; eauto.
-  exploit Val.modu_divu; eauto. intros [v [A B]].
-  subst. econstructor; split; eauto.
-  apply eval_mod_aux with (semdivop := Val.divu); auto.
+  intros. unfold shrximm. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  subst n. exists x; split; auto. 
+  destruct x; simpl in H0; try discriminate.
+  destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
+  replace (Int.shrx i Int.zero) with i. auto. 
+  unfold Int.shrx, Int.divs. rewrite Int.shl_zero. 
+  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+  econstructor; split. EvalOp. auto.
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
diff --git a/test/regression/Results/int32 b/test/regression/Results/int32
index e0fafc4..1223a5b 100644
--- a/test/regression/Results/int32
+++ b/test/regression/Results/int32
@@ -8,6 +8,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = ffffffff
 x & y = 0
 x | y = 0
@@ -32,6 +44,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = ffffffff
 x & y = 0
 x | y = 1
@@ -56,6 +80,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = ffffffff
 x & y = 0
 x | y = ffffffff
@@ -80,6 +116,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = ffffffff
 x & y = 0
 x | y = 7fffffff
@@ -104,6 +152,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = ffffffff
 x & y = 0
 x | y = 80000000
@@ -128,6 +188,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = ffffffff
 x & y = 0
 x | y = 6255
@@ -152,6 +224,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 0
+x /u 3 = 228b7b22
+x %u 3 = 0
+x /s 3 = 228b7b22
+x %s 3 = 0
+x /u 5 = 14ba16ae
+x %u 5 = 0
+x /s 5 = 14ba16ae
+x %s 5 = 0
+x /u 11 = 96bdbc3
+x %u 11 = 5
+x /s 11 = 96bdbc3
+x %s 11 = 5
 ~x = 985d8e99
 x & y = 0
 x | y = 67a27166
@@ -176,6 +260,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = fffffffe
 x & y = 0
 x | y = 1
@@ -200,6 +296,18 @@ x /u y = 1
 x %u y = 0
 x /s y = 1
 x %s y = 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 = fffffffe
 x & y = 1
 x | y = 1
@@ -224,6 +332,18 @@ x /u y = 0
 x %u y = 1
 x /s y = ffffffff
 x %s y = 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 = fffffffe
 x & y = 1
 x | y = ffffffff
@@ -248,6 +368,18 @@ x /u y = 0
 x %u y = 1
 x /s y = 0
 x %s y = 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 = fffffffe
 x & y = 1
 x | y = 7fffffff
@@ -272,6 +404,18 @@ x /u y = 0
 x %u y = 1
 x /s y = 0
 x %s y = 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 = fffffffe
 x & y = 0
 x | y = 80000001
@@ -296,6 +440,18 @@ x /u y = 0
 x %u y = 1
 x /s y = 0
 x %s y = 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 = fffffffe
 x & y = 1
 x | y = ae3d5f03
@@ -320,6 +476,18 @@ x /u y = 3fb9ebc
 x %u y = 0
 x /s y = 3fb9ebc
 x %s y = 0
+x /u 3 = 153df94
+x %u 3 = 0
+x /s 3 = 153df94
+x %s 3 = 0
+x /u 5 = cbec8c
+x %u 5 = 0
+x /s 5 = cbec8c
+x %s 5 = 0
+x /u 11 = 5cb156
+x %u 11 = a
+x /s 11 = 5cb156
+x %s 11 = a
 ~x = fc046143
 x & y = 0
 x | y = 3fb9ebd
@@ -344,6 +512,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 0
+x /u 3 = 55555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffff
+x /u 5 = 33333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffff
+x /u 11 = 1745d174
+x %u 11 = 3
+x /s 11 = 0
+x %s 11 = ffffffff
 ~x = 0
 x & y = 0
 x | y = ffffffff
@@ -368,6 +548,18 @@ x /u y = ffffffff
 x %u y = 0
 x /s y = ffffffff
 x %s y = 0
+x /u 3 = 55555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffff
+x /u 5 = 33333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffff
+x /u 11 = 1745d174
+x %u 11 = 3
+x /s 11 = 0
+x %s 11 = ffffffff
 ~x = 0
 x & y = 1
 x | y = ffffffff
@@ -392,6 +584,18 @@ x /u y = 1
 x %u y = 0
 x /s y = 1
 x %s y = 0
+x /u 3 = 55555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffff
+x /u 5 = 33333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffff
+x /u 11 = 1745d174
+x %u 11 = 3
+x /s 11 = 0
+x %s 11 = ffffffff
 ~x = 0
 x & y = ffffffff
 x | y = ffffffff
@@ -416,6 +620,18 @@ x /u y = 2
 x %u y = 1
 x /s y = 0
 x %s y = ffffffff
+x /u 3 = 55555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffff
+x /u 5 = 33333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffff
+x /u 11 = 1745d174
+x %u 11 = 3
+x /s 11 = 0
+x %s 11 = ffffffff
 ~x = 0
 x & y = 7fffffff
 x | y = ffffffff
@@ -440,6 +656,18 @@ x /u y = 1
 x %u y = 7fffffff
 x /s y = 0
 x %s y = ffffffff
+x /u 3 = 55555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffff
+x /u 5 = 33333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffff
+x /u 11 = 1745d174
+x %u 11 = 3
+x /s 11 = 0
+x %s 11 = ffffffff
 ~x = 0
 x & y = 80000000
 x | y = ffffffff
@@ -464,6 +692,18 @@ x /u y = 1
 x %u y = 69b5f51e
 x /s y = 0
 x %s y = ffffffff
+x /u 3 = 55555555
+x %u 3 = 0
+x /s 3 = 0
+x %s 3 = ffffffff
+x /u 5 = 33333333
+x %u 5 = 0
+x /s 5 = 0
+x %s 5 = ffffffff
+x /u 11 = 1745d174
+x %u 11 = 3
+x /s 11 = 0
+x %s 11 = ffffffff
 ~x = 0
 x & y = 964a0ae1
 x | y = ffffffff
@@ -488,6 +728,18 @@ x /u y = 0
 x %u y = 26b98582
 x /s y = d9467a7e
 x %s y = 0
+x /u 3 = ce881d6
+x %u 3 = 0
+x /s 3 = ce881d6
+x %s 3 = 0
+x /u 5 = 7beb44d
+x %u 5 = 1
+x /s 5 = 7beb44d
+x %s 5 = 1
+x /u 11 = 3853aae
+x %u 11 = 8
+x /s 11 = 3853aae
+x %s 11 = 8
 ~x = d9467a7d
 x & y = 26b98582
 x | y = ffffffff
@@ -512,6 +764,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 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 = 80000000
 x & y = 0
 x | y = 7fffffff
@@ -536,6 +800,18 @@ x /u y = 7fffffff
 x %u y = 0
 x /s y = 7fffffff
 x %s y = 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 = 80000000
 x & y = 1
 x | y = 7fffffff
@@ -560,6 +836,18 @@ x /u y = 0
 x %u y = 7fffffff
 x /s y = 80000001
 x %s y = 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 = 80000000
 x & y = 7fffffff
 x | y = ffffffff
@@ -584,6 +872,18 @@ x /u y = 1
 x %u y = 0
 x /s y = 1
 x %s y = 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 = 80000000
 x & y = 7fffffff
 x | y = 7fffffff
@@ -608,6 +908,18 @@ x /u y = 0
 x %u y = 7fffffff
 x /s y = 0
 x %s y = 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 = 80000000
 x & y = 0
 x | y = ffffffff
@@ -632,6 +944,18 @@ x /u y = 0
 x %u y = 7fffffff
 x /s y = fffffff6
 x %s y = 682f655
+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 = 80000000
 x & y = 73d9e56f
 x | y = ffffffff
@@ -656,6 +980,18 @@ x /u y = 0
 x %u y = 3b92bf38
 x /s y = 0
 x %s y = 3b92bf38
+x /u 3 = 13db9512
+x %u 3 = 2
+x /s 3 = 13db9512
+x %s 3 = 2
+x /u 5 = bea263e
+x %u 5 = 2
+x /s 5 = bea263e
+x %s 5 = 2
+x /u 11 = 56a6e79
+x %u 11 = 5
+x /s 11 = 56a6e79
+x %s 11 = 5
 ~x = c46d40c7
 x & y = 3b92bf38
 x | y = 7fffffff
@@ -680,6 +1016,18 @@ x /u y = 0
 x %u y = 0
 x /s y = 0
 x %s y = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = d5555556
+x %s 3 = fffffffe
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = e6666667
+x %s 5 = fffffffd
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = f45d1746
+x %s 11 = fffffffe
 ~x = 7fffffff
 x & y = 0
 x | y = 80000000
@@ -704,6 +1052,18 @@ x /u y = 80000000
 x %u y = 0
 x /s y = 80000000
 x %s y = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = d5555556
+x %s 3 = fffffffe
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = e6666667
+x %s 5 = fffffffd
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = f45d1746
+x %s 11 = fffffffe
 ~x = 7fffffff
 x & y = 0
 x | y = 80000001
@@ -728,6 +1088,18 @@ x /u y = 0
 x %u y = 80000000
 x /s y = 0
 x %s y = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = d5555556
+x %s 3 = fffffffe
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = e6666667
+x %s 5 = fffffffd
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = f45d1746
+x %s 11 = fffffffe
 ~x = 7fffffff
 x & y = 80000000
 x | y = ffffffff
@@ -752,6 +1124,18 @@ x /u y = 1
 x %u y = 1
 x /s y = ffffffff
 x %s y = ffffffff
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = d5555556
+x %s 3 = fffffffe
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = e6666667
+x %s 5 = fffffffd
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = f45d1746
+x %s 11 = fffffffe
 ~x = 7fffffff
 x & y = 0
 x | y = ffffffff
@@ -776,6 +1160,18 @@ x /u y = 1
 x %u y = 0
 x /s y = 1
 x %s y = 0
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = d5555556
+x %s 3 = fffffffe
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = e6666667
+x %s 5 = fffffffd
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = f45d1746
+x %s 11 = fffffffe
 ~x = 7fffffff
 x & y = 80000000
 x | y = 80000000
@@ -800,6 +1196,18 @@ x /u y = 0
 x %u y = 80000000
 x /s y = 5
 x %s y = fac93d1f
+x /u 3 = 2aaaaaaa
+x %u 3 = 2
+x /s 3 = d5555556
+x %s 3 = fffffffe
+x /u 5 = 19999999
+x %u 5 = 3
+x /s 5 = e6666667
+x %s 5 = fffffffd
+x /u 11 = ba2e8ba
+x %u 11 = 2
+x /s 11 = f45d1746
+x %s 11 = fffffffe
 ~x = 7fffffff
 x & y = 80000000
 x | y = e7715a2d
@@ -824,6 +1232,18 @@ x /u y = 0
 x %u y = 7186e15e
 x /s y = 0
 x %s y = 7186e15e
+x /u 3 = 25d7a074
+x %u 3 = 2
+x /s 3 = 25d7a074
+x %s 3 = 2
+x /u 5 = 16b49379
+x %u 5 = 1
+x /s 5 = 16b49379
+x %s 5 = 1
+x /u 11 = a52147c
+x %u 11 = a
+x /s 11 = a52147c
+x %s 11 = a
 ~x = 8e791ea1
 x & y = 0
 x | y = f186e15e
@@ -848,6 +1268,18 @@ x /u y = 1
 x %u y = 2164c327
 x /s y = 0
 x %s y = a3d2a09b
+x /u 3 = 369b8ade
+x %u 3 = 1
+x /s 3 = e1463589
+x %s 3 = 0
+x /u 5 = 20c3b9b8
+x %u 5 = 3
+x /s 5 = ed908686
+x %s 5 = fffffffd
+x /u 11 = ee49a3c
+x %u 11 = 7
+x /s 11 = f79ec8c9
+x %s 11 = fffffff8
 ~x = 5c2d5f64
 x & y = 82408010
 x | y = a3fffdff
@@ -872,6 +1304,18 @@ x /u y = 1
 x %u y = 247f3b3f
 x /s y = 0
 x %s y = e3ad9c39
+x /u 3 = 4be48968
+x %u 3 = 1
+x /s 3 = f68f3413
+x %s 3 = 0
+x /u 5 = 2d891f3e
+x %u 5 = 3
+x /s 5 = fa55ec0c
+x %s 5 = fffffffd
+x /u 11 = 14b2b11c
+x %u 11 = 5
+x /s 11 = fd6cdfa9
+x %s 11 = fffffff6
 ~x = 1c5263c6
 x & y = a32c0038
 x | y = ffaffcfb
@@ -896,6 +1340,18 @@ x /u y = a
 x %u y = 50aa627
 x /s y = fffffffe
 x %s y = fd712767
+x /u 3 = 46ae3ed7
+x %u 3 = 2
+x /s 3 = f158e983
+x %s 3 = fffffffe
+x /u 5 = 2a688c1b
+x %u 5 = 0
+x /s 5 = f73558e8
+x %s 5 = ffffffff
+x /u 11 = 1346cb52
+x %u 11 = 1
+x /s 11 = fc00f9de
+x %s 11 = fffffffd
 ~x = 2bf54378
 x & y = 14023400
 x | y = d4bbbdf7
@@ -920,6 +1376,18 @@ x /u y = 0
 x %u y = e2a8dd05
 x /s y = 2
 x %s y = ffb99c59
+x /u 3 = 4b8d9f01
+x %u 3 = 2
+x /s 3 = f63849ad
+x %s 3 = fffffffe
+x /u 5 = 2d54f901
+x %u 5 = 0
+x /s 5 = fa21c5ce
+x %s 5 = ffffffff
+x /u 11 = 149afcd1
+x %u 11 = a
+x /s 11 = fd552b5e
+x %s 11 = fffffffb
 ~x = 1d5722fa
 x & y = e0208004
 x | y = f3fffd57
@@ -944,6 +1412,18 @@ x /u y = 0
 x %u y = 10462533
 x /s y = 0
 x %s y = 10462533
+x /u 3 = 56cb711
+x %u 3 = 0
+x /s 3 = 56cb711
+x %s 3 = 0
+x /u 5 = 3413aa3
+x %u 5 = 4
+x /s 5 = 3413aa3
+x %s 5 = 4
+x /u 11 = 17abd90
+x %u 11 = 3
+x /s 11 = 17abd90
+x %s 11 = 3
 ~x = efb9dacc
 x & y = 10420120
 x | y = bd46e73f
@@ -968,6 +1448,18 @@ x /u y = 1
 x %u y = 5121ed1f
 x /s y = 0
 x %s y = b58be891
+x /u 3 = 3c83f830
+x %u 3 = 1
+x /s 3 = e72ea2db
+x %s 3 = 0
+x /u 5 = 244f2e83
+x %u 5 = 2
+x /s 5 = f11bfb51
+x %s 5 = fffffffc
+x /u 11 = 10811524
+x %u 11 = 5
+x /s 11 = f93b43b1
+x %s 11 = fffffff6
 ~x = 4a74176e
 x & y = 2409e810
 x | y = f5ebfbf3
@@ -992,6 +1484,18 @@ x /u y = 3
 x %u y = cfebea7
 x /s y = 0
 x %s y = c615869f
+x /u 3 = 42072cdf
+x %u 3 = 2
+x /s 3 = ecb1d78b
+x %s 3 = fffffffe
+x /u 5 = 279de7b9
+x %u 5 = 2
+x /s 5 = f46ab487
+x %s 5 = fffffffc
+x /u 11 = 1201f4f7
+x %u 11 = 2
+x /s 11 = fabc2383
+x %s 11 = fffffffe
 ~x = 39ea7960
 x & y = 4100288
 x | y = ffb7c6bf
@@ -1016,6 +1520,18 @@ x /u y = 0
 x %u y = b7ca4add
 x /s y = 1
 x %s y = fa21bc8f
+x /u 3 = 3d436e49
+x %u 3 = 2
+x /s 3 = e7ee18f5
+x %s 3 = fffffffe
+x /u 5 = 24c20ef9
+x %u 5 = 0
+x /s 5 = f18edbc6
+x %s 5 = ffffffff
+x /u 11 = 10b54c9f
+x %u 11 = 8
+x /s 11 = f96f7b2c
+x %s 11 = fffffff9
 ~x = 4835b522
 x & y = b5880a4c
 x | y = bfeacedf
@@ -1040,6 +1556,18 @@ x /u y = 1
 x %u y = 11791ce7
 x /s y = 0
 x %s y = fd824ccb
+x /u 3 = 5480c443
+x %u 3 = 2
+x /s 3 = ff2b6eef
+x %s 3 = fffffffe
+x /u 5 = 32b3a8f5
+x %u 5 = 2
+x /s 5 = ff8075c3
+x %s 5 = fffffffc
+x /u 11 = 170bd86f
+x %u 11 = 6
+x /s 11 = ffc606fc
+x %s 11 = fffffff7
 ~x = 27db334
 x & y = ec000cc0
 x | y = fd8b6fef
@@ -1064,6 +1592,18 @@ x /u y = 0
 x %u y = aaae4fe9
 x /s y = 2
 x %s y = fb91e615
+x /u 3 = 38e4c54d
+x %u 3 = 2
+x /s 3 = e38f6ff9
+x %s 3 = fffffffe
+x /u 5 = 2222dcc8
+x %u 5 = 1
+x /s 5 = eeefa995
+x %s 5 = 0
+x /u 11 = f8435cf
+x %u 11 = 4
+x /s 11 = f83e645b
+x %s 11 = 0
 ~x = 5551b016
 x & y = 828e04e8
 x | y = ffae7feb
@@ -1088,6 +1628,18 @@ x /u y = 0
 x %u y = a7aa3b7
 x /s y = 0
 x %s y = a7aa3b7
+x /u 3 = 37e3692
+x %u 3 = 1
+x /s 3 = 37e3692
+x %s 3 = 1
+x /u 5 = 2188724
+x %u 5 = 3
+x /s 5 = 2188724
+x %s 5 = 3
+x /u 11 = f3e056
+x %u 11 = 5
+x /s 11 = f3e056
+x %s 11 = 5
 ~x = f5855c48
 x & y = 23882a0
 x | y = 4a7ee7f7
@@ -1112,6 +1664,18 @@ x /u y = 1
 x %u y = 39b786f
 x /s y = 0
 x %s y = e7a503b5
+x /u 3 = 4d37013c
+x %u 3 = 1
+x /s 3 = f7e1abe7
+x %s 3 = 0
+x /u 5 = 2e5433f1
+x %u 5 = 0
+x /s 5 = fb2100be
+x %s 5 = ffffffff
+x /u 11 = 150f0056
+x %u 11 = 3
+x /s 11 = fdc92ee2
+x %s 11 = ffffffff
 ~x = 185afc4a
 x & y = e4010304
 x | y = e7ad8bf7
@@ -1136,6 +1700,18 @@ x /u y = 0
 x %u y = a2fd7763
 x /s y = 2
 x %s y = ec25702b
+x /u 3 = 36547d21
+x %u 3 = 0
+x /s 3 = e0ff27cc
+x %s 3 = ffffffff
+x /u 5 = 209917e0
+x %u 5 = 3
+x /s 5 = ed65e4ae
+x %s 5 = fffffffd
+x /u 11 = ed13966
+x %u 11 = 1
+x /s 11 = f78b67f2
+x %s 11 = fffffffd
 ~x = 5d02889c
 x & y = 826c0300
 x | y = fbfd77ff
@@ -1160,6 +1736,18 @@ x /u y = 0
 x %u y = 354a3241
 x /s y = 0
 x %s y = 354a3241
+x /u 3 = 11c36615
+x %u 3 = 2
+x /s 3 = 11c36615
+x %s 3 = 2
+x /u 5 = aa87073
+x %u 5 = 2
+x /s 5 = aa87073
+x %s 5 = 2
+x /u 11 = 4d8331d
+x %u 11 = 2
+x /s 11 = 4d8331d
+x %s 11 = 2
 ~x = cab5cdbe
 x & y = 21082040
 x | y = b77aff63
@@ -1184,6 +1772,18 @@ x /u y = 4
 x %u y = 1a97eb6f
 x /s y = fffffffc
 x %s y = f174fc2f
+x /u 3 = 2cacd145
+x %u 3 = 0
+x /s 3 = d7577bf0
+x %s 3 = ffffffff
+x /u 5 = 1ace1729
+x %u 5 = 2
+x /s 5 = e79ae3f7
+x %s 5 = fffffffc
+x /u 11 = c2f21cd
+x %u 11 = 0
+x /s 11 = f4e95059
+x %s 11 = fffffffc
 ~x = 79f98c30
 x & y = 2022208
 x | y = 9edff3df
@@ -1208,6 +1808,18 @@ x /u y = 1
 x %u y = 16df04f
 x /s y = 1
 x %s y = 16df04f
+x /u 3 = 191177d9
+x %u 3 = 2
+x /s 3 = 191177d9
+x %s 3 = 2
+x /u 5 = f0a7b1c
+x %u 5 = 1
+x /s 5 = f0a7b1c
+x %s 5 = 1
+x /u 11 = 6d637f5
+x %u 11 = 6
+x /s 11 = 6d637f5
+x %s 11 = 6
 ~x = b4cb9872
 x & y = 4904670c
 x | y = 4bf677bf
@@ -1232,6 +1844,18 @@ x /u y = 1
 x %u y = 2687e6a7
 x /s y = 0
 x %s y = 9f3a04fb
+x /u 3 = 351356fe
+x %u 3 = 1
+x /s 3 = dfbe01a9
+x %s 3 = 0
+x /u 5 = 1fd86765
+x %u 5 = 2
+x /s 5 = eca53433
+x %s 5 = fffffffc
+x /u 11 = e79a35c
+x %u 11 = 7
+x /s 11 = f733d1e9
+x %s 11 = fffffff8
 ~x = 60c5fb04
 x & y = 18320450
 x | y = ffba1eff
@@ -1256,6 +1880,18 @@ x /u y = 1
 x %u y = 5d7ceabf
 x /s y = 0
 x %s y = d080ef99
+x /u 3 = 45804fdd
+x %u 3 = 2
+x /s 3 = f02afa89
+x %s 3 = fffffffe
+x /u 5 = 29b3631e
+x %u 5 = 3
+x /s 5 = f6802fec
+x %s 5 = fffffffd
+x /u 11 = 12f472df
+x %u 11 = 4
+x /s 11 = fbaea16b
+x %s 11 = 0
 ~x = 2f7f1066
 x & y = 50000498
 x | y = f384efdb
@@ -1280,6 +1916,18 @@ x /u y = 1
 x %u y = 22dda297
 x /s y = 1
 x %s y = 22dda297
+x /u 3 = 1bc5c7a2
+x %u 3 = 1
+x /s 3 = 1bc5c7a2
+x %s 3 = 1
+x /u 5 = 10a9de2e
+x %u 5 = 1
+x /s 5 = 10a9de2e
+x %s 5 = 1
+x /u 11 = 79307e6
+x %u 11 = 5
+x /s 11 = 79307e6
+x %s 11 = 5
 ~x = acaea918
 x & y = 10511440
 x | y = 7373f6f7
@@ -1304,6 +1952,18 @@ x /u y = 1
 x %u y = 2658a42f
 x /s y = 1
 x %s y = 2658a42f
+x /u 3 = 205ff221
+x %u 3 = 2
+x /s 3 = 205ff221
+x %s 3 = 2
+x /u 5 = 136cc47a
+x %u 5 = 3
+x /s 5 = 136cc47a
+x %s 5 = 3
+x /u 11 = 8d4594f
+x %u 11 = 0
+x /s 11 = 8d4594f
+x %s 11 = 0
 ~x = 9ee0299a
 x & y = 20071224
 x | y = 7bdff677
@@ -1328,6 +1988,18 @@ x /u y = 0
 x %u y = 61465593
 x /s y = ffffffff
 x %s y = 2e84b59f
+x /u 3 = 206cc731
+x %u 3 = 0
+x /s 3 = 206cc731
+x %s 3 = 0
+x /u 5 = 13747783
+x %u 5 = 4
+x /s 5 = 13747783
+x %s 5 = 4
+x /u 11 = 8d7d93b
+x %u 11 = a
+x /s 11 = 8d7d93b
+x %s 11 = a
 ~x = 9eb9aa6c
 x & y = 41064000
 x | y = ed7e759f
@@ -1352,6 +2024,18 @@ x /u y = 2
 x %u y = 2fd5314d
 x /s y = 0
 x %s y = e5dfe7f1
+x /u 3 = 4c9ff7fb
+x %u 3 = 0
+x /s 3 = f74aa2a6
+x %s 3 = ffffffff
+x /u 5 = 2df994c9
+x %u 5 = 4
+x /s 5 = fac66197
+x %s 5 = fffffffe
+x /u 11 = 14e5cf44
+x %u 11 = 5
+x /s 11 = fd9ffdd1
+x %s 11 = fffffff6
 ~x = 1a20180e
 x & y = 41054350
 x | y = ffdffff3
@@ -1376,6 +2060,18 @@ x /u y = 0
 x %u y = 843facff
 x /s y = 2
 x %s y = e4b3f1ef
+x /u 3 = 2c1539aa
+x %u 3 = 1
+x /s 3 = d6bfe455
+x %s 3 = 0
+x /u 5 = 1a732299
+x %u 5 = 2
+x /s 5 = e73fef67
+x %s 5 = fffffffc
+x /u 11 = c05c9e8
+x %u 11 = 7
+x /s 11 = f4bff875
+x %s 11 = fffffff8
 ~x = 7bc05300
 x & y = 84058c88
 x | y = cffffdff
@@ -1400,6 +2096,18 @@ x /u y = 0
 x %u y = 4b3ab03d
 x /s y = fffffffd
 x %s y = 6c984c7
+x /u 3 = 19139014
+x %u 3 = 1
+x /s 3 = 19139014
+x %s 3 = 1
+x /u 5 = f0bbcd9
+x %u 5 = 0
+x /s 5 = f0bbcd9
+x %s 5 = 0
+x /u 11 = 6d6ca34
+x %u 11 = 1
+x /s 11 = 6d6ca34
+x %s 11 = 1
 ~x = b4c54fc2
 x & y = 492a902c
 x | y = eb3fbc3f
@@ -1424,6 +2132,18 @@ x /u y = 1
 x %u y = 582d2067
 x /s y = 0
 x %s y = c23cc92b
+x /u 3 = 40beedb9
+x %u 3 = 0
+x /s 3 = eb699864
+x %s 3 = ffffffff
+x /u 5 = 26d8f508
+x %u 5 = 3
+x /s 5 = f3a5c1d6
+x %s 5 = fffffffd
+x /u 11 = 11a86f61
+x %u 11 = 0
+x /s 11 = fa629ded
+x %s 11 = fffffffc
 ~x = 3dc336d4
 x & y = 420c8800
 x | y = ea3fe9ef
@@ -1448,6 +2168,18 @@ x /u y = 6
 x %u y = 707968d
 x /s y = 6
 x %s y = 707968d
+x /u 3 = 20f57e6d
+x %u 3 = 2
+x /s 3 = 20f57e6d
+x %s 3 = 2
+x /u 5 = 13c67f0e
+x %u 5 = 3
+x /s 5 = 13c67f0e
+x %s 5 = 3
+x /u 11 = 8fd227b
+x %u 11 = 0
+x /s 11 = 8fd227b
+x %s 11 = 0
 ~x = 9d1f84b6
 x & y = 2405048
 x | y = 6feefbcb
@@ -1472,6 +2204,18 @@ x /u y = 1
 x %u y = 692d857
 x /s y = 1
 x %s y = 692d857
+x /u 3 = 6809cb2
+x %u 3 = 1
+x /s 3 = 6809cb2
+x %s 3 = 1
+x /u 5 = 3e6c46b
+x %u 5 = 0
+x /s 5 = 3e6c46b
+x %s 5 = 0
+x /u 11 = 1c5fc30
+x %u 11 = 7
+x /s 11 = 1c5fc30
+x %s 11 = 7
 ~x = ec7e29e8
 x & y = 80d400
 x | y = 1fefffd7
@@ -1496,6 +2240,18 @@ x /u y = 0
 x %u y = 7c045515
 x /s y = fffffffd
 x %s y = 12a31487
+x /u 3 = 2956c707
+x %u 3 = 0
+x /s 3 = 2956c707
+x %s 3 = 0
+x /u 5 = 18cdaa9d
+x %u 5 = 4
+x /s 5 = 18cdaa9d
+x %s 5 = 4
+x /u 11 = b463647
+x %u 11 = 8
+x /s 11 = b463647
+x %s 11 = 8
 ~x = 83fbaaea
 x & y = 5c041504
 x | y = fcdfd537
@@ -1520,6 +2276,18 @@ x /u y = 3
 x %u y = 501364f
 x /s y = 0
 x %s y = cec3bfc3
+x /u 3 = 44ebea96
+x %u 3 = 1
+x /s 3 = ef969541
+x %s 3 = 0
+x /u 5 = 295a598d
+x %u 5 = 2
+x /s 5 = f627265b
+x %s 5 = fffffffc
+x /u 11 = 12cbfa29
+x %u 11 = 0
+x /s 11 = fb8628b5
+x %s 11 = fffffffc
 ~x = 313c403c
 x & y = 42409840
 x | y = cfc3ffff
@@ -1544,6 +2312,18 @@ x /u y = 16
 x %u y = 2ee15f5
 x /s y = 0
 x %s y = fe6809a1
+x /u 3 = 54cd588b
+x %u 3 = 0
+x /s 3 = ff780336
+x %s 3 = ffffffff
+x /u 5 = 32e19b86
+x %u 5 = 3
+x /s 5 = ffae6854
+x %s 5 = fffffffd
+x /u 11 = 1720bb0e
+x %u 11 = 7
+x /s 11 = ffdae99b
+x %s 11 = fffffff8
 ~x = 197f65e
 x & y = a680100
 x | y = ff6e4de3
@@ -1568,6 +2348,18 @@ x /u y = 0
 x %u y = 614322f
 x /s y = 0
 x %s y = 614322f
+x /u 3 = 206bb65
+x %u 3 = 0
+x /s 3 = 206bb65
+x %s 3 = 0
+x /u 5 = 1373d3c
+x %u 5 = 3
+x /s 5 = 1373d3c
+x %s 5 = 3
+x /u 11 = 8d78ed
+x %u 11 = 0
+x /s 11 = 8d78ed
+x %s 11 = 0
 ~x = f9ebcdd0
 x & y = 6043028
 x | y = 16f7f6ff
@@ -1592,6 +2384,18 @@ x /u y = 0
 x %u y = 142824ed
 x /s y = 0
 x %s y = 142824ed
+x /u 3 = 6b80c4f
+x %u 3 = 0
+x /s 3 = 6b80c4f
+x %s 3 = 0
+x /u 5 = 4080762
+x %u 5 = 3
+x /s 5 = 4080762
+x %s 5 = 3
+x /u 11 = 1d51aa1
+x %u 11 = 2
+x /s 11 = 1d51aa1
+x %s 11 = 2
 ~x = ebd7db12
 x & y = 1020240c
 x | y = 56fafdff
@@ -1616,6 +2420,18 @@ x /u y = 0
 x %u y = c08d995b
 x /s y = e
 x %s y = ff124483
+x /u 3 = 402f331e
+x %u 3 = 1
+x /s 3 = ead9ddc9
+x %s 3 = 0
+x /u 5 = 2682b845
+x %u 5 = 2
+x /s 5 = f34f8513
+x %s 5 = fffffffc
+x /u 11 = 11813c7c
+x %u 11 = 7
+x /s 11 = fa3b6b09
+x %s 11 = fffffff8
 ~x = 3f7266a4
 x & y = c0888910
 x | y = fb8ddf7f
@@ -1640,6 +2456,18 @@ x /u y = 0
 x %u y = 2e47f2f9
 x /s y = 0
 x %s y = 2e47f2f9
+x /u 3 = f6d50fd
+x %u 3 = 2
+x /s 3 = f6d50fd
+x %s 3 = 2
+x /u 5 = 94196fe
+x %u 5 = 3
+x /s 5 = 94196fe
+x %s 5 = 3
+x /u 11 = 4351616
+x %u 11 = 7
+x /s 11 = 4351616
+x %s 11 = 7
 ~x = d1b80d06
 x & y = 284590b8
 x | y = afeffafb
@@ -1664,6 +2492,18 @@ x /u y = 0
 x %u y = bcbf2147
 x /s y = d
 x %s y = fd75d7d7
+x /u 3 = 3eea606d
+x %u 3 = 0
+x /s 3 = e9950b18
+x %s 3 = ffffffff
+x /u 5 = 25bfd374
+x %u 5 = 3
+x /s 5 = f28ca042
+x %s 5 = fffffffd
+x /u 11 = 1128a5ef
+x %u 11 = 2
+x /s 11 = f9e2d47b
+x %s 11 = fffffffe
 ~x = 4340deb8
 x & y = b8052100
 x | y = ffbfa377
@@ -1688,6 +2528,18 @@ x /u y = 1
 x %u y = 62bbcbaf
 x /s y = 0
 x %s y = effd7fc5
+x /u 3 = 4fff2a97
+x %u 3 = 0
+x /s 3 = faa9d542
+x %s 3 = ffffffff
+x /u 5 = 2fff7ff4
+x %u 5 = 1
+x /s 5 = fccc4cc1
+x %s 5 = 0
+x /u 11 = 15d13a29
+x %u 11 = 2
+x /s 11 = fe8b68b5
+x %s 11 = fffffffe
 ~x = 1002803a
 x & y = 8d413404
 x | y = effdffd7
@@ -1712,6 +2564,18 @@ x /u y = 0
 x %u y = 27d8b5f3
 x /s y = 0
 x %s y = 27d8b5f3
+x /u 3 = d483ca6
+x %u 3 = 1
+x /s 3 = d483ca6
+x %s 3 = 1
+x /u 5 = 7f82463
+x %u 5 = 4
+x /s 5 = 7f82463
+x %s 5 = 4
+x /u 11 = 39f565b
+x %u 11 = a
+x /s 11 = 39f565b
+x %s 11 = a
 ~x = d8274a0c
 x & y = 79824e0
 x | y = bffafdff
@@ -1736,6 +2600,18 @@ x /u y = 4
 x %u y = 1d72ea89
 x /s y = ffffffff
 x %s y = f8904283
+x /u 3 = 443f3270
+x %u 3 = 1
+x /s 3 = eee9dd1b
+x %s 3 = 0
+x /u 5 = 28f2b7dd
+x %u 5 = 0
+x /s 5 = f5bf84aa
+x %s 5 = ffffffff
+x /u 11 = 129cdf35
+x %u 11 = a
+x /s 11 = fb570dc2
+x %s 11 = fffffffb
 ~x = 334268ae
 x & y = 8908310
 x | y = efffbf73
@@ -1760,6 +2636,18 @@ x /u y = 0
 x %u y = 7597035f
 x /s y = fffffffe
 x %s y = 2688d42f
+x /u 3 = 27325675
+x %u 3 = 0
+x /s 3 = 27325675
+x %s 3 = 0
+x /u 5 = 17849a46
+x %u 5 = 1
+x /s 5 = 17849a46
+x %s 5 = 1
+x /u 11 = ab0a337
+x %u 11 = 2
+x /s 11 = ab0a337
+x %s 11 = 2
 ~x = 8a68fca0
 x & y = 50100048
 x | y = fdffeb7f
@@ -1784,6 +2672,18 @@ x /u y = 5
 x %u y = ba9c357
 x /s y = 5
 x %s y = ba9c357
+x /u 3 = 21ad41df
+x %u 3 = 0
+x /s 3 = 21ad41df
+x %s 3 = 0
+x /u 5 = 1434c11f
+x %u 5 = 2
+x /s 5 = 1434c11f
+x %s 5 = 2
+x /u 11 = 92f4082
+x %u 11 = 7
+x /s 11 = 92f4082
+x %s 11 = 7
 ~x = 9af83a62
 x & y = 107800c
 x | y = 75dfdf9f
@@ -1808,6 +2708,18 @@ x /u y = 0
 x %u y = 44ef758b
 x /s y = ffffffff
 x %s y = 1734072f
+x /u 3 = 16fa7c83
+x %u 3 = 2
+x /s 3 = 16fa7c83
+x %s 3 = 2
+x /u 5 = dc97de8
+x %u 5 = 3
+x /s 5 = dc97de8
+x %s 5 = 3
+x /u 11 = 6445081
+x %u 11 = 0
+x /s 11 = 6445081
+x %s 11 = 0
 ~x = bb108a74
 x & y = 40441180
 x | y = d6eff5af
@@ -1832,6 +2744,18 @@ x /u y = 0
 x %u y = 6df256a9
 x /s y = ffffffff
 x %s y = 1e11b353
+x /u 3 = 24a61ce3
+x %u 3 = 0
+x /s 3 = 24a61ce3
+x %s 3 = 0
+x /u 5 = 15fd4488
+x %u 5 = 1
+x /s 5 = 15fd4488
+x %s 5 = 1
+x /u 11 = 9fec20f
+x %u 11 = 4
+x /s 11 = 9fec20f
+x %s 11 = 4
 ~x = 920da956
 x & y = 201254a8
 x | y = fdff5eab
@@ -1856,6 +2780,18 @@ x /u y = 1
 x %u y = 79ad93d7
 x /s y = 0
 x %s y = fd7c3877
+x /u 3 = 547ebd7d
+x %u 3 = 0
+x /s 3 = ff296828
+x %s 3 = ffffffff
+x /u 5 = 32b271b1
+x %u 5 = 2
+x /s 5 = ff7f3e7f
+x %s 5 = fffffffc
+x /u 11 = 170b4af3
+x %u 11 = 6
+x /s 11 = ffc57980
+x %s 11 = fffffff7
 ~x = 283c788
 x & y = 814c2020
 x | y = fffebcf7
@@ -1880,6 +2816,18 @@ x /u y = 0
 x %u y = af765675
 x /s y = 2
 x %s y = fa3d3869
+x /u 3 = 3a7cc77c
+x %u 3 = 1
+x /s 3 = e5277227
+x %s 3 = 0
+x /u 5 = 2317aae4
+x %u 5 = 1
+x /s 5 = efe477b1
+x %s 5 = 0
+x /u 11 = ff37c39
+x %u 11 = 2
+x /s 11 = f8adaac5
+x %s 11 = fffffffe
 ~x = 5089a98a
 x & y = 8a140604
 x | y = fffedf77
@@ -1904,6 +2852,18 @@ x /u y = 1
 x %u y = 2af61ac7
 x /s y = ffffffff
 x %s y = f85a557f
+x /u 3 = 308d680b
+x %u 3 = 2
+x /s 3 = db3812b7
+x %s 3 = fffffffe
+x /u 5 = 1d21a4d3
+x %u 5 = 4
+x /s 5 = e9ee71a1
+x %s 5 = fffffffe
+x /u 11 = d3dd68e
+x %u 11 = 9
+x /s 11 = f5f8051b
+x %s 11 = fffffffa
 ~x = 6e57c7dc
 x & y = a01800
 x | y = f7ba3d7f
@@ -1928,6 +2888,18 @@ x /u y = 3
 x %u y = 1386e99b
 x /s y = 3
 x %s y = 1386e99b
+x /u 3 = 21d3db00
+x %u 3 = 1
+x /s 3 = 21d3db00
+x %s 3 = 1
+x /u 5 = 144be9cd
+x %u 5 = 0
+x /s 5 = 144be9cd
+x %s 5 = 0
+x /u 11 = 939c75d
+x %u 11 = 2
+x /s 11 = 939c75d
+x %s 11 = 2
 ~x = 9a846efe
 x & y = 1518100
 x | y = 7f7b9d23
@@ -1952,6 +2924,18 @@ x /u y = 0
 x %u y = 919b208f
 x /s y = 1
 x %s y = f72b68b7
+x /u 3 = 30890ada
+x %u 3 = 1
+x /s 3 = db33b585
+x %s 3 = 0
+x /u 5 = 1d1f0683
+x %u 5 = 0
+x /s 5 = e9ebd350
+x %s 5 = ffffffff
+x /u 11 = d3ca5de
+x %u 11 = 5
+x /s 11 = f5f6d46b
+x %s 11 = fffffff6
 ~x = 6e64df70
 x & y = 900b2088
 x | y = 9bffb7df
@@ -1976,6 +2960,18 @@ x /u y = 0
 x %u y = fa4924d
 x /s y = 0
 x %s y = fa4924d
+x /u 3 = 536db6f
+x %u 3 = 0
+x /s 3 = 536db6f
+x %s 3 = 0
+x /u 5 = 320ea0f
+x %u 5 = 2
+x /s 5 = 320ea0f
+x %s 5 = 2
+x /u 11 = 16c0d4c
+x %u 11 = 9
+x /s 11 = 16c0d4c
+x %s 11 = 9
 ~x = f05b6db2
 x & y = 484124c
 x | y = 7fa4f2ff
@@ -2000,6 +2996,18 @@ x /u y = 1
 x %u y = dbb6da7
 x /s y = 1
 x %s y = dbb6da7
+x /u 3 = 28f71f3e
+x %u 3 = 1
+x /s 3 = 28f71f3e
+x %s 3 = 1
+x /u 5 = 189445f2
+x %u 5 = 1
+x /s 5 = 189445f2
+x %s 5 = 1
+x /u 11 = b2c1fcb
+x %u 11 = 2
+x /s 11 = b2c1fcb
+x %s 11 = 2
 ~x = 851aa244
 x & y = 68215010
 x | y = 7fedfdbf
@@ -2024,6 +3032,18 @@ x /u y = 0
 x %u y = 7bdaa659
 x /s y = fffffff9
 x %s y = 4106e8f
+x /u 3 = 2948e21d
+x %u 3 = 2
+x /s 3 = 2948e21d
+x %s 3 = 2
+x /u 5 = 18c55478
+x %u 5 = 1
+x /s 5 = 18c55478
+x %s 5 = 1
+x /u 11 = b426c36
+x %u 11 = 7
+x /s 11 = b426c36
+x %s 11 = 7
 ~x = 842559a6
 x & y = 6ac20418
 x | y = fffbbedb
@@ -2048,6 +3068,18 @@ x /u y = 27
 x %u y = 1e4cb37
 x /s y = fffffffe
 x %s y = fd2e1fc7
+x /u 3 = 504eb3e2
+x %u 3 = 1
+x /s 3 = faf95e8d
+x %s 3 = 0
+x /u 5 = 302f38bb
+x %u 5 = 0
+x /s 5 = fcfc0588
+x %s 5 = ffffffff
+x /u 11 = 15e6eb3d
+x %u 11 = 8
+x /s 11 = fea119ca
+x %s 11 = fffffff9
 ~x = f13e458
 x & y = 200200
 x | y = f6ed1bb7
@@ -2072,6 +3104,18 @@ x /u y = 9
 x %u y = d41837f
 x /s y = fffffffa
 x %s y = f3d4bce9
+x /u 3 = 32889db7
+x %u 3 = 0
+x /s 3 = dd334862
+x %s 3 = ffffffff
+x /u 5 = 1e51f83a
+x %u 5 = 3
+x /s 5 = eb1ec508
+x %s 5 = fffffffd
+x /u 11 = dc82b03
+x %u 11 = 4
+x /s 11 = f682598f
+x %s 11 = 0
 ~x = 686626da
 x & y = 7190124
 x | y = 9fdffdf7
@@ -2096,6 +3140,18 @@ x /u y = 0
 x %u y = 4a154653
 x /s y = 0
 x %s y = 4a154653
+x /u 3 = 18b1c21b
+x %u 3 = 2
+x /s 3 = 18b1c21b
+x %s 3 = 2
+x /u 5 = ed10e10
+x %u 5 = 3
+x /s 5 = ed10e10
+x %s 5 = 3
+x /u 11 = 6bc1daa
+x %u 11 = 5
+x /s 11 = 6bc1daa
+x %s 11 = 5
 ~x = b5eab9ac
 x & y = 8044040
 x | y = efffefdf
@@ -2120,6 +3176,18 @@ x /u y = 5
 x %u y = b5f57
 x /s y = 5
 x %s y = b5f57
+x /u 3 = 1bfefce5
+x %u 3 = 2
+x /s 3 = 1bfefce5
+x %s 3 = 2
+x /u 5 = 10cc3156
+x %u 5 = 3
+x /s 5 = 10cc3156
+x %s 5 = 3
+x /u 11 = 7a2a210
+x %u 11 = 1
+x /s 11 = 7a2a210
+x %s 11 = 1
 ~x = ac03094e
 x & y = 10c8e210
 x | y = 53fdffb3
@@ -2144,6 +3212,18 @@ x /u y = 0
 x %u y = 9db389bf
 x /s y = 6
 x %s y = fa9f360f
+x /u 3 = 34912dea
+x %u 3 = 1
+x /s 3 = df3bd895
+x %s 3 = 0
+x /u 5 = 1f8a4ebf
+x %u 5 = 4
+x /s 5 = ec571b8d
+x %s 5 = fffffffe
+x /u 11 = e5623cb
+x %u 11 = 6
+x /s 11 = f7105258
+x %s 11 = fffffff7
 ~x = 624c7640
 x & y = 90830108
 x | y = fdb3ebff
@@ -2168,6 +3248,18 @@ x /u y = 1
 x %u y = 2b59030f
 x /s y = 0
 x %s y = a8898afd
+x /u 3 = 382dd8ff
+x %u 3 = 0
+x /s 3 = e2d883aa
+x %s 3 = ffffffff
+x /u 5 = 21b51bcc
+x %u 5 = 1
+x /s 5 = ee81e899
+x %s 5 = 0
+x /u 11 = f525274
+x %u 11 = 1
+x /s 11 = f80c8100
+x %s 11 = fffffffd
 ~x = 57767502
 x & y = 280082ec
 x | y = fdb98fff
@@ -2192,6 +3284,18 @@ x /u y = 0
 x %u y = 3eb251eb
 x /s y = 0
 x %s y = 3eb251eb
+x /u 3 = 14e61b4e
+x %u 3 = 1
+x /s 3 = 14e61b4e
+x %s 3 = 1
+x /u 5 = c8a1062
+x %u 5 = 1
+x /s 5 = c8a1062
+x %s 5 = 1
+x /u 11 = 5b31eb8
+x %u 11 = 3
+x /s 11 = 5b31eb8
+x %s 11 = 3
 ~x = c14dae14
 x & y = 14924080
 x | y = befffbef
@@ -2216,6 +3320,18 @@ x /u y = 0
 x %u y = 80bbe209
 x /s y = 1
 x %s y = fdc4097f
+x /u 3 = 2ae94b58
+x %u 3 = 1
+x /s 3 = d593f603
+x %s 3 = 0
+x /u 5 = 19bf2d35
+x %u 5 = 0
+x /s 5 = e68bfa02
+x %s 5 = ffffffff
+x /u 11 = bb3fd46
+x %u 11 = 7
+x /s 11 = f46e2bd3
+x %s 11 = fffffff8
 ~x = 7f441df6
 x & y = 80b3c008
 x | y = 82fffa8b
@@ -2240,6 +3356,18 @@ x /u y = 2
 x %u y = 1da53d7
 x /s y = 2
 x %s y = 1da53d7
+x /u 3 = 1a55ee47
+x %u 3 = 2
+x /s 3 = 1a55ee47
+x %s 3 = 2
+x /u 5 = fcd2891
+x %u 5 = 2
+x /s 5 = fcd2891
+x %s 5 = 2
+x /u 11 = 72eb559
+x %u 11 = 4
+x /s 11 = 72eb559
+x %s 11 = 4
 ~x = b0fe3528
 x & y = 6018a80
 x | y = 6f93fbd7
@@ -2264,6 +3392,18 @@ x /u y = 0
 x %u y = 205307d5
 x /s y = 0
 x %s y = 205307d5
+x /u 3 = ac657f1
+x %u 3 = 2
+x /s 3 = ac657f1
+x %s 3 = 2
+x /u 5 = 6770191
+x %u 5 = 0
+x /s 5 = 6770191
+x %s 5 = 0
+x /u 11 = 2f04687
+x %u 11 = 8
+x /s 11 = 2f04687
+x %s 11 = 8
 ~x = dfacf82a
 x & y = 201000c4
 x | y = 21fb7ff7
@@ -2288,6 +3428,18 @@ x /u y = 1
 x %u y = 4acb0e47
 x /s y = 0
 x %s y = d7c2e083
+x /u 3 = 47eba02b
+x %u 3 = 2
+x /s 3 = f2964ad7
+x %s 3 = fffffffe
+x /u 5 = 2b26f9b3
+x %u 5 = 4
+x /s 5 = f7f3c681
+x %s 5 = fffffffe
+x /u 11 = 139d5a3a
+x %u 11 = 5
+x /s 11 = fc5788c7
+x %s 11 = fffffff6
 ~x = 283d1f7c
 x & y = 84c2c000
 x | y = dff7f2bf
@@ -2312,6 +3464,18 @@ x /u y = 6
 x %u y = 93c2a55
 x /s y = 6
 x %s y = 93c2a55
+x /u 3 = 18c99820
+x %u 3 = 1
+x /s 3 = 18c99820
+x %s 3 = 1
+x /u 5 = edf5b46
+x %u 5 = 3
+x /s 5 = edf5b46
+x %s 5 = 3
+x /u 11 = 6c29dda
+x %u 11 = 3
+x /s 11 = 6c29dda
+x %s 11 = 3
 ~x = b5a3379e
 x & y = a58c000
 x | y = 4adecd63
@@ -2336,6 +3500,18 @@ x /u y = 0
 x %u y = 92333eef
 x /s y = 5
 x %s y = f55ca957
+x /u 3 = 30bbbfa5
+x %u 3 = 0
+x /s 3 = db666a50
+x %s 3 = ffffffff
+x /u 5 = 1d3d72fc
+x %u 5 = 3
+x /s 5 = ea0a3fca
+x %s 5 = fffffffd
+x /u 11 = d4a7a15
+x %u 11 = 8
+x /s 11 = f604a8a2
+x %s 11 = fffffff9
 ~x = 6dccc110
 x & y = 80222aa8
 x | y = fe3bfeff
@@ -2360,6 +3536,18 @@ x /u y = 0
 x %u y = 3701afad
 x /s y = ffffffff
 x %s y = 8f4888b
+x /u 3 = 1255e539
+x %u 3 = 2
+x /s 3 = 1255e539
+x %s 3 = 2
+x /u 5 = b005655
+x %u 5 = 4
+x /s 5 = b005655
+x %s 5 = 4
+x /u 11 = 500273e
+x %u 11 = 3
+x /s 11 = 500273e
+x %s 11 = 3
 ~x = c8fe5052
 x & y = 1100888c
 x | y = f7f3ffff
@@ -2384,6 +3572,18 @@ x /u y = 0
 x %u y = 4d59521b
 x /s y = ffffffff
 x %s y = 1926d30f
+x /u 3 = 19c870b3
+x %u 3 = 2
+x /s 3 = 19c870b3
+x %s 3 = 2
+x /u 5 = f78439f
+x %u 5 = 0
+x /s 5 = f78439f
+x %s 5 = 0
+x /u 11 = 7081ebc
+x %u 11 = 7
+x /s 11 = 7081ebc
+x %s 11 = 7
 ~x = b2a6ade4
 x & y = 49490010
 x | y = cfddd2ff
@@ -2408,6 +3608,18 @@ x /u y = 0
 x %u y = 241109b9
 x /s y = 0
 x %s y = 241109b9
+x /u 3 = c05ade8
+x %u 3 = 1
+x /s 3 = c05ade8
+x %s 3 = 1
+x /u 5 = 7369b8b
+x %u 5 = 2
+x /s 5 = 7369b8b
+x %s 5 = 2
+x /u 11 = 3475df9
+x %u 11 = 6
+x /s 11 = 3475df9
+x %s 11 = 6
 ~x = dbeef646
 x & y = 100038
 x | y = ecdd99fb
@@ -2432,6 +3644,18 @@ x /u y = 2
 x %u y = 1d74a427
 x /s y = ffffffff
 x %s y = dbee16f7
+x /u 3 = 34256cad
+x %u 3 = 0
+x /s 3 = ded01758
+x %s 3 = ffffffff
+x /u 5 = 1f49a79b
+x %u 5 = 0
+x /s 5 = ec167468
+x %s 5 = ffffffff
+x /u 11 = e38c08c
+x %u 11 = 3
+x /s 11 = f6f2ef18
+x %s 11 = ffffffff
 ~x = 638fb9f8
 x & y = 1c704000
 x | y = bf7dd6f7
@@ -2456,6 +3680,18 @@ x /u y = 0
 x %u y = c4ce285
 x /s y = 0
 x %s y = c4ce285
+x /u 3 = 419a0d7
+x %u 3 = 0
+x /s 3 = 419a0d7
+x %s 3 = 0
+x /u 5 = 275c6e7
+x %u 5 = 2
+x /s 5 = 275c6e7
+x %s 5 = 2
+x /u 11 = 11e4323
+x %u 11 = 4
+x /s 11 = 11e4323
+x %s 11 = 4
 ~x = f3b31d7a
 x & y = 48284
 x | y = afdfe7d7
@@ -2480,6 +3716,18 @@ x /u y = 0
 x %u y = 3a1406b3
 x /s y = 0
 x %s y = 3a1406b3
+x /u 3 = 135c023b
+x %u 3 = 2
+x /s 3 = 135c023b
+x %s 3 = 2
+x /u 5 = b9d9af0
+x %u 5 = 3
+x /s 5 = b9d9af0
+x %s 5 = 3
+x /u 11 = 547a384
+x %u 11 = 7
+x /s 11 = 547a384
+x %s 11 = 7
 ~x = c5ebf94c
 x & y = 81006a0
 x | y = bf17d6bf
@@ -2504,6 +3752,18 @@ x /u y = 1
 x %u y = 1192eb1f
 x /s y = 0
 x %s y = d1760611
+x /u 3 = 45d20205
+x %u 3 = 2
+x /s 3 = f07cacb1
+x %s 3 = fffffffe
+x /u 5 = 29e4679d
+x %u 5 = 0
+x /s 5 = f6b1346a
+x %s 5 = ffffffff
+x /u 11 = 130ababb
+x %u 11 = 8
+x /s 11 = fbc4e948
+x %s 11 = fffffff9
 ~x = 2e89f9ee
 x & y = 91620210
 x | y = fff71ef3
@@ -2528,6 +3788,18 @@ x /u y = 0
 x %u y = 4c2d401f
 x /s y = 0
 x %s y = 4c2d401f
+x /u 3 = 19646ab5
+x %u 3 = 0
+x /s 3 = 19646ab5
+x %s 3 = 0
+x /u 5 = f3c4006
+x %u 5 = 1
+x /s 5 = f3c4006
+x %s 5 = 1
+x /u 11 = 6ecd748
+x %u 11 = 7
+x /s 11 = 6ecd748
+x %s 11 = 7
 ~x = b3d2bfe0
 x & y = c0d4008
 x | y = ccbd4e3f
@@ -2552,6 +3824,18 @@ x /u y = 1
 x %u y = 387d9a8f
 x /s y = 0
 x %s y = e518005d
+x /u 3 = 4c5d5574
+x %u 3 = 1
+x /s 3 = f708001f
+x %s 3 = 0
+x /u 5 = 2dd199ac
+x %u 5 = 1
+x /s 5 = fa9e6679
+x %s 5 = 0
+x /u 11 = 14d3a2f1
+x %u 11 = 2
+x /s 11 = fd8dd17d
+x %s 11 = fffffffe
 ~x = 1ae7ffa2
 x & y = a418004c
 x | y = ed9a65df
@@ -2576,6 +3860,18 @@ x /u y = 0
 x %u y = 749d5e4b
 x /s y = ffffffff
 x %s y = 32b711af
+x /u 3 = 26df1f6e
+x %u 3 = 1
+x /s 3 = 26df1f6e
+x %s 3 = 1
+x /u 5 = 1752ac75
+x %u 5 = 2
+x /s 5 = 1752ac75
+x %s 5 = 2
+x /u 11 = a99f14c
+x %u 11 = 7
+x /s 11 = a99f14c
+x %s 11 = 7
 ~x = 8b62a1b4
 x & y = 34191240
 x | y = fe9dff6f
@@ -2600,6 +3896,18 @@ x /u y = 0
 x %u y = 3c151d69
 x /s y = 0
 x %s y = 3c151d69
+x /u 3 = 140709cd
+x %u 3 = 2
+x /s 3 = 140709cd
+x %s 3 = 2
+x /u 5 = c043915
+x %u 5 = 0
+x /s 5 = c043915
+x %s 5 = 0
+x /u 11 = 576487d
+x %u 11 = a
+x /s 11 = 576487d
+x %s 11 = a
 ~x = c3eae296
 x & y = c100468
 x | y = 7cd55d6b
@@ -2624,6 +3932,18 @@ x /u y = 0
 x %u y = 5aaa8d37
 x /s y = ffffffff
 x %s y = 2ba0cf97
+x /u 3 = 1e38d9bd
+x %u 3 = 0
+x /s 3 = 1e38d9bd
+x %s 3 = 0
+x /u 5 = 12221c3e
+x %u 5 = 1
+x /s 5 = 12221c3e
+x %s 5 = 1
+x /u 11 = 83e0cd6
+x %u 11 = 5
+x /s 11 = 83e0cd6
+x %s 11 = 5
 ~x = a55572c8
 x & y = 50a20020
 x | y = dafecf77
@@ -2648,6 +3968,18 @@ x /u y = 0
 x %u y = 18f26935
 x /s y = 0
 x %s y = 18f26935
+x /u 3 = 850cdbc
+x %u 3 = 1
+x /s 3 = 850cdbc
+x %s 3 = 1
+x /u 5 = 4fd483d
+x %u 5 = 4
+x /s 5 = 4fd483d
+x %s 5 = 4
+x /u 11 = 2449533
+x %u 11 = 4
+x /s 11 = 2449533
+x %s 11 = 4
 ~x = e70d96ca
 x & y = 10a24004
 x | y = bafb7bf7
@@ -2672,6 +4004,18 @@ x /u y = 0
 x %u y = 192bb8e3
 x /s y = 0
 x %s y = 192bb8e3
+x /u 3 = 863e84b
+x %u 3 = 2
+x /s 3 = 863e84b
+x %s 3 = 2
+x /u 5 = 508be93
+x %u 5 = 4
+x /s 5 = 508be93
+x %s 5 = 4
+x /u 11 = 249cafd
+x %u 11 = 4
+x /s 11 = 249cafd
+x %s 11 = 4
 ~x = e6d4471c
 x & y = 1909b000
 x | y = 196bffff
@@ -2696,6 +4040,18 @@ x /u y = 1
 x %u y = 6ae1c2df
 x /s y = 0
 x %s y = f8e3afc1
+x /u 3 = 52f68feb
+x %u 3 = 0
+x /s 3 = fda13a96
+x %s 3 = ffffffff
+x /u 5 = 31c72326
+x %u 5 = 3
+x /s 5 = fe93eff4
+x %s 5 = fffffffd
+x /u 11 = 16a055cb
+x %u 11 = 8
+x /s 11 = ff5a8458
+x %s 11 = fffffff9
 ~x = 71c503e
 x & y = 8801acc0
 x | y = fee3efe3
@@ -2720,6 +4076,18 @@ x /u y = 4
 x %u y = 22e56ef
 x /s y = ffffffff
 x %s y = ec461ae7
+x /u 3 = 3f26d9c5
+x %u 3 = 0
+x /s 3 = e9d18470
+x %s 3 = ffffffff
+x /u 5 = 25e41c43
+x %u 5 = 0
+x /s 5 = f2b0e910
+x %s 5 = ffffffff
+x /u 11 = 1139241e
+x %u 11 = 5
+x /s 11 = f9f352ab
+x %s 11 = fffffff6
 ~x = 428b72b0
 x & y = 2c508d08
 x | y = bff58ddf
@@ -2744,6 +4112,18 @@ x /u y = 0
 x %u y = af977d0d
 x /s y = 1
 x %s y = e4e14e4f
+x /u 3 = 3a87d459
+x %u 3 = 2
+x /s 3 = e5327f05
+x %s 3 = fffffffe
+x /u 5 = 231e4c35
+x %u 5 = 4
+x /s 5 = efeb1903
+x %s 5 = fffffffe
+x /u 11 = ff67fbb
+x %u 11 = 4
+x /s 11 = f8b0ae47
+x %s 11 = 0
 ~x = 506882f2
 x & y = 8a962c0c
 x | y = efb77fbf
@@ -2768,6 +4148,18 @@ x /u y = 1
 x %u y = 1155f4a7
 x /s y = 0
 x %s y = c301767b
+x /u 3 = 41007cd3
+x %u 3 = 2
+x /s 3 = ebab277f
+x %s 3 = fffffffe
+x /u 5 = 27004ae5
+x %u 5 = 2
+x /s 5 = f3cd17b3
+x %s 5 = fffffffc
+x /u 11 = 11ba5096
+x %u 11 = 9
+x /s 11 = fa747f23
+x %s 11 = fffffffa
 ~x = 3cfe8984
 x & y = 81010050
 x | y = f3abf7ff
@@ -2792,6 +4184,18 @@ x /u y = 0
 x %u y = 7dc31d19
 x /s y = ffffffff
 x %s y = 38951173
+x /u 3 = 29ebb45d
+x %u 3 = 2
+x /s 3 = 29ebb45d
+x %s 3 = 2
+x /u 5 = 192705d1
+x %u 5 = 4
+x /s 5 = 192705d1
+x %s 5 = 4
+x /u 11 = b6ed419
+x %u 11 = 6
+x /s 11 = b6ed419
+x %s 11 = 6
 ~x = 823ce2e6
 x & y = 38c11418
 x | y = ffd3fd5b
@@ -2816,6 +4220,18 @@ x /u y = 0
 x %u y = 37e3a067
 x /s y = fffffffd
 x %s y = a5fcfd7
+x /u 3 = 12a13577
+x %u 3 = 2
+x /s 3 = 12a13577
+x %s 3 = 2
+x /u 5 = b2d867b
+x %u 5 = 0
+x /s 5 = b2d867b
+x %s 5 = 0
+x /u 11 = 514b17d
+x %u 11 = 8
+x /s 11 = 514b17d
+x %s 11 = 8
 ~x = c81c5f98
 x & y = 30c00040
 x | y = f7f7aff7
@@ -2840,6 +4256,18 @@ x /u y = 0
 x %u y = ae6e9be5
 x /s y = 3
 x %s y = f5460ec3
+x /u 3 = 3a24dea1
+x %u 3 = 2
+x /s 3 = e4cf894d
+x %s 3 = fffffffe
+x /u 5 = 22e2ebfa
+x %u 5 = 3
+x /s 5 = efafb8c8
+x %s 5 = fffffffd
+x /u 11 = fdb8289
+x %u 11 = 2
+x /s 11 = f895b115
+x %s 11 = fffffffe
 ~x = 5191641a
 x & y = a86299a4
 x | y = ee6edbf7
@@ -2864,6 +4292,18 @@ x /u y = 1
 x %u y = 78bc387
 x /s y = 0
 x %s y = f5ecf713
+x /u 3 = 51f9a7b1
+x %u 3 = 0
+x /s 3 = fca4525c
+x %s 3 = ffffffff
+x /u 5 = 312f649d
+x %u 5 = 2
+x /s 5 = fdfc316b
+x %s 5 = fffffffc
+x /u 11 = 165b5c47
+x %u 11 = 6
+x /s 11 = ff158ad4
+x %s 11 = fffffff7
 ~x = a1308ec
 x & y = e4603300
 x | y = ffedf79f
@@ -2888,6 +4328,18 @@ x /u y = 0
 x %u y = 700c571
 x /s y = 0
 x %s y = 700c571
+x /u 3 = 2559725
+x %u 3 = 2
+x /s 3 = 2559725
+x %s 3 = 2
+x /u 5 = 1668de3
+x %u 5 = 2
+x /s 5 = 1668de3
+x %s 5 = 2
+x /u 11 = a2faad
+x %u 11 = 2
+x /s 11 = a2faad
+x %s 11 = 2
 ~x = f8ff3a8e
 x & y = 3000050
 x | y = 6f16fff3
@@ -2912,6 +4364,18 @@ x /u y = 0
 x %u y = 1c9c267f
 x /s y = fffffff5
 x %s y = 10d69d7
+x /u 3 = 989622a
+x %u 3 = 1
+x /s 3 = 989622a
+x %s 3 = 1
+x /u 5 = 5b8d47f
+x %u 5 = 4
+x /s 5 = 5b8d47f
+x %s 5 = 4
+x /u 11 = 299d4f4
+x %u 11 = 3
+x /s 11 = 299d4f4
+x %s 11 = 3
 ~x = e363d980
 x & y = 1c1c2008
 x | y = fdfeaf7f
@@ -2936,6 +4400,18 @@ x /u y = 0
 x %u y = 160b25bd
 x /s y = 0
 x %s y = 160b25bd
+x /u 3 = 7590c94
+x %u 3 = 1
+x /s 3 = 7590c94
+x %s 3 = 1
+x /u 5 = 468a125
+x %u 5 = 4
+x /s 5 = 468a125
+x %s 5 = 4
+x /u 11 = 201036e
+x %u 11 = 3
+x /s 11 = 201036e
+x %s 11 = 3
 ~x = e9f4da42
 x & y = 140121ac
 x | y = 5f9f37bf
@@ -2960,6 +4436,18 @@ x /u y = 0
 x %u y = b7c89aab
 x /s y = 7
 x %s y = fca324cf
+x /u 3 = 3d42de39
+x %u 3 = 0
+x /s 3 = e7ed88e4
+x %s 3 = ffffffff
+x /u 5 = 24c1b888
+x %u 5 = 3
+x /s 5 = f18e8556
+x %s 5 = fffffffd
+x /u 11 = 10b52555
+x %u 11 = 4
+x /s 11 = f96f53e1
+x %s 11 = 0
 ~x = 48376554
 x & y = b6088800
 x | y = f7e9feef
@@ -2984,6 +4472,18 @@ x /u y = 0
 x %u y = 2cd608c9
 x /s y = 0
 x %s y = 2cd608c9
+x /u 3 = ef202ed
+x %u 3 = 2
+x /s 3 = ef202ed
+x %s 3 = 2
+x /u 5 = 8f79b5b
+x %u 5 = 2
+x /s 5 = 8f79b5b
+x %s 5 = 2
+x /u 11 = 4137529
+x %u 11 = 6
+x /s 11 = 4137529
+x %s 11 = 6
 ~x = d329f736
 x & y = c800048
 x | y = eef6a8cb
@@ -3008,6 +4508,18 @@ x /u y = 0
 x %u y = 3f0e7f97
 x /s y = 0
 x %s y = 3f0e7f97
+x /u 3 = 1504d532
+x %u 3 = 1
+x /s 3 = 1504d532
+x %s 3 = 1
+x /u 5 = c9c7feb
+x %u 5 = 0
+x /s 5 = c9c7feb
+x %s 5 = 0
+x /u 11 = 5bb7ff6
+x %u 11 = 5
+x /s 11 = 5bb7ff6
+x %s 11 = 5
 ~x = c0f18068
 x & y = 3a0e3900
 x | y = bfae7fd7
@@ -3032,6 +4544,18 @@ x /u y = 1
 x %u y = 45bf5def
 x /s y = ffffffff
 x %s y = d999973b
+x /u 3 = 2fe428dc
+x %u 3 = 1
+x /s 3 = da8ed387
+x %s 3 = 0
+x /u 5 = 1cbc1884
+x %u 5 = 1
+x /s 5 = e988e551
+x %s 5 = 0
+x /u 11 = d0fae0d
+x %u 11 = 6
+x /s 11 = f5c9dc9a
+x %s 11 = fffffff7
 ~x = 7053856a
 x & y = 9ac1884
 x | y = cfed7eb7
@@ -3056,6 +4580,18 @@ x /u y = 0
 x %u y = 59fac143
 x /s y = 0
 x %s y = 59fac143
+x /u 3 = 1dfe406b
+x %u 3 = 2
+x /s 3 = 1dfe406b
+x %s 3 = 2
+x /u 5 = 11fef373
+x %u 5 = 4
+x /s 5 = 11fef373
+x %s 5 = 4
+x /u 11 = 82e1191
+x %u 11 = 8
+x /s 11 = 82e1191
+x %s 11 = 8
 ~x = a6053ebc
 x & y = 8e08140
 x | y = dbfacbff
@@ -3080,6 +4616,18 @@ x /u y = 0
 x %u y = 28e84721
 x /s y = 0
 x %s y = 28e84721
+x /u 3 = da2c260
+x %u 3 = 1
+x /s 3 = da2c260
+x %s 3 = 1
+x /u 5 = 82e74a0
+x %u 5 = 1
+x /s 5 = 82e74a0
+x %s 5 = 1
+x /u 11 = 3b80677
+x %u 11 = 4
+x /s 11 = 3b80677
+x %s 11 = 4
 ~x = d717b8de
 x & y = a80400
 x | y = fcff47e3
@@ -3104,6 +4652,18 @@ x /u y = 0
 x %u y = 14f70baf
 x /s y = 0
 x %s y = 14f70baf
+x /u 3 = 6fd03e5
+x %u 3 = 0
+x /s 3 = 6fd03e5
+x %s 3 = 0
+x /u 5 = 43168bc
+x %u 5 = 3
+x /s 5 = 43168bc
+x %s 5 = 3
+x /u 11 = 1e7e9ca
+x %u 11 = 1
+x /s 11 = 1e7e9ca
+x %s 11 = 1
 ~x = eb08f450
 x & y = 130028
 x | y = 75ffabff
@@ -3128,6 +4688,18 @@ x /u y = 0
 x %u y = cabdfa6d
 x /s y = 9
 x %s y = fe43e0df
+x /u 3 = 4394a8cf
+x %u 3 = 0
+x /s 3 = ee3f537a
+x %s 3 = ffffffff
+x /u 5 = 288c6549
+x %u 5 = 0
+x /s 5 = f5593216
+x %s 5 = ffffffff
+x /u 11 = 126e5c95
+x %u 11 = 6
+x /s 11 = fb288b22
+x %s 11 = fffffff7
 ~x = 35420592
 x & y = ca04700c
 x | y = fafffeff
@@ -3152,6 +4724,18 @@ x /u y = 1
 x %u y = 1df9d827
 x /s y = 1
 x %s y = 1df9d827
+x /u 3 = 2651ee49
+x %u 3 = 0
+x /s 3 = 2651ee49
+x %s 3 = 0
+x /u 5 = 16fdf55f
+x %u 5 = 0
+x /s 5 = 16fdf55f
+x %s 5 = 0
+x /u 11 = a736f88
+x %u 11 = 3
+x /s 11 = a736f88
+x %s 11 = 3
 ~x = 8d0a3524
 x & y = 50f1c290
 x | y = 76fffaff
@@ -3176,6 +4760,18 @@ x /u y = 3
 x %u y = 9707cb
 x /s y = 0
 x %s y = cbc8e079
+x /u 3 = 43eda028
+x %u 3 = 1
+x /s 3 = ee984ad3
+x %s 3 = 0
+x /u 5 = 28c1c67e
+x %u 5 = 3
+x /s 5 = f58e934c
+x %s 5 = fffffffd
+x /u 11 = 1286a00b
+x %u 11 = 0
+x /s 11 = fb40ce97
+x %s 11 = fffffffc
 ~x = 34371f86
 x & y = 43884038
 x | y = cbfbe87b
@@ -3200,6 +4796,18 @@ x /u y = 0
 x %u y = 7de2ac7
 x /s y = 0
 x %s y = 7de2ac7
+x /u 3 = 29f6397
+x %u 3 = 2
+x /s 3 = 29f6397
+x %s 3 = 2
+x /u 5 = 192d55b
+x %u 5 = 0
+x /s 5 = 192d55b
+x %s 5 = 0
+x /u 11 = b71b29
+x %u 11 = 4
+x /s 11 = b71b29
+x %s 11 = 4
 ~x = f821d538
 x & y = 7da2a80
 x | y = bfdfbef7
@@ -3224,6 +4832,18 @@ x /u y = 2
 x %u y = 19e4ce19
 x /s y = fffffffe
 x %s y = fac93c71
+x /u 3 = 2e1d01c1
+x %u 3 = 2
+x /s 3 = d8c7ac6d
+x %s 3 = fffffffe
+x /u 5 = 1bab010d
+x %u 5 = 4
+x /s 5 = e877cddb
+x %s 5 = fffffffe
+x /u 11 = c938c1d
+x %u 11 = 6
+x /s 11 = f54dbaaa
+x %s 11 = fffffff7
 ~x = 75a8faba
 x & y = 8110104
 x | y = ba7f1fd7
diff --git a/test/regression/int32.c b/test/regression/int32.c
index bec50f0..d7b6c9e 100644
--- a/test/regression/int32.c
+++ b/test/regression/int32.c
@@ -48,6 +48,18 @@ static void test1(u32 x, u32 y)
   printf("x %%u y = %x\n", safe_umod32(x, y));
   printf("x /s y = %x\n", safe_sdiv32(x, y));
   printf("x %%s y = %x\n", safe_smod32(x, y));
+  printf("x /u 3 = %x\n", x / 3);
+  printf("x %%u 3 = %x\n", x % 3);
+  printf("x /s 3 = %x\n", (s32)x / 3);
+  printf("x %%s 3 = %x\n", (s32)x % 3);
+  printf("x /u 5 = %x\n", x / 5);
+  printf("x %%u 5 = %x\n", x % 5);
+  printf("x /s 5 = %x\n", (s32)x / 5);
+  printf("x %%s 5 = %x\n", (s32)x % 5);
+  printf("x /u 11 = %x\n", x / 11);
+  printf("x %%u 11 = %x\n", x % 11);
+  printf("x /s 11 = %x\n", (s32)x / 11);
+  printf("x %%s 11 = %x\n", (s32)x % 11);
   printf("~x = %x\n", ~x);
   printf("x & y = %x\n", x & y);
   printf("x | y = %x\n", x | y);