diff --git a/manticore/native/cpu/x86.py b/manticore/native/cpu/x86.py
index e839d7268..a43dbbdd1 100644
--- a/manticore/native/cpu/x86.py
+++ b/manticore/native/cpu/x86.py
@@ -961,6 +961,10 @@ def CPUID(cpu):
                 0x0: (0x00000000, 0x00000000, 0x00000000, 0x00000000),
                 0x1: (0x00000000, 0x00000000, 0x00000000, 0x00000000),
             },
+            # CPUID with EAX=80000000h returns the highest supported extended function
+            # query in EAX. We don't currently support any other than 80000000h itself,
+            # so just return it back.
+            0x80000000: (0x80000000, 0x00000000, 0x00000000, 0x00000000),
         }
 
         if cpu.EAX not in conf: