diff --git a/arch/alpha/vtophys.cc b/arch/alpha/vtophys.cc
index f4b2c7ed3..464ed41e6 100644
--- a/arch/alpha/vtophys.cc
+++ b/arch/alpha/vtophys.cc
@@ -100,11 +100,11 @@ vtophys(ExecContext *xc, Addr vaddr)
     //so I put it back in. Perhaps something to do with gdb debugging?
     if (PC_PAL(vaddr)) {
         paddr = vaddr & ~ULL(1);
-    } else if (!ptbr) {
-        paddr = vaddr;
     } else {
         if (vaddr >= ALPHA_K0SEG_BASE && vaddr <= ALPHA_K0SEG_END) {
             paddr = ALPHA_K0SEG_TO_PHYS(vaddr);
+        } else if (!ptbr) {
+            paddr = vaddr;
         } else {
             Addr pte = kernel_pte_lookup(xc->physmem, ptbr, vaddr);
             uint64_t entry = xc->physmem->phys_read_qword(pte);