diff --git a/Changelog.md b/Changelog.md
index 453c92911..5ed65e600 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -12,6 +12,7 @@ Bug fixes:
 - Thread the current typing environment through `Elab.elab_initializer`.
 - Printing of assembly files: quote command-line arguments when needed (#586)
 - Printing of assembly files: revised string quoting in debugging information (#588)
+- x86 64 bits, `Pjmptbl` instruction: make sure the 32-bit argument is zero-extended to 64 bits before indexing in the jump table (#595)
 
 Usability:
 - AArch64 asm clobbers: recognize more register names (#576)
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index f4cea9dda..6e38ec1ae 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -521,6 +521,7 @@ module Target : TARGET =
          fprintf oc "	flw	%a, %a, x31 %s %.18g\n"
                     freg rd label lbl comment (camlfloat_of_coqfloat32 f)
       | Pbtbl(r, tbl) ->
+         assert (Int64.of_int (List.length tbl) <= 0x8000_0000L);
          let lbl = new_label() in
          fprintf oc "%s jumptable [ " comment;
          List.iter (fun l -> fprintf oc "%a " print_label l) tbl;
diff --git a/test b/test
index 27899bbab..4df7312a3 160000
--- a/test
+++ b/test
@@ -1 +1 @@
-Subproject commit 27899bbabecd10148c2a2f1b3b62f55b8edca556
+Subproject commit 4df7312a3ff71037c20856dfeff727e36c77848e
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 3bc863f7d..397ebe78b 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -752,7 +752,9 @@ module Target(System: SYSTEM):TARGET =
             let (tmp1, tmp2) =
               if r = RAX then (RDX, RAX) else (RAX, RDX) in
             fprintf oc "	leaq	%a(%%rip), %a\n" label l ireg tmp1;
-            fprintf oc "	movslq	(%a, %a, 4), %a\n" ireg tmp1 ireg r ireg tmp2;
+            (* Normalize r to 32-bit unsigned *)
+            fprintf oc "	movl	%a, %a\n" ireg32 r ireg32 tmp2;
+            fprintf oc "	movslq	(%a, %a, 4), %a\n" ireg tmp1 ireg tmp2 ireg tmp2;
             fprintf oc "	addq	%a, %a\n" ireg tmp2 ireg tmp1;
             fprintf oc "	jmp	*%a\n" ireg tmp1
           end else begin