1 files changed, 5 insertions, 1 deletions
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 70941c48..72a6e4b3 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -742,7 +742,7 @@ Nondetfunction gen_fmaf args :=
   | _ => None
   end.
 
-Require FPDivision32.
+Require FPDivision32 FPDivision64.
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
   match b with
@@ -758,6 +758,10 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
                      | a:::b:::Enil => Some (FPDivision32.fp_divu32 a b)
                      | _ => None
                      end)
+  | BI_fp_udiv64 => (match args with
+                     | a:::b:::Enil => Some (FPDivision64.fp_divu64 a b)
+                     | _ => None
+                     end)
   end.
 End SELECT.