diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index b1bfcef88..c3e9fb182 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -220,7 +220,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
                     _            => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
                   };
                   match (eares) {
-                    MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
+                    MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
                     MemValue(_) => {
                       rs2_val = X(rs2);
                       let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
@@ -233,7 +233,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
                       match (res) {
                         MemValue(true)  => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
                         MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
-                        MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
+                        MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
                       }
                     }
                   }
@@ -303,7 +303,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
               DOUBLE => X(rs2)
             };
             match (eares) {
-              MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
+              MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
               MemValue(_) => {
                 let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
                   (BYTE, _)    => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)),
@@ -313,7 +313,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                   _            => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
                 };
                 match (mval) {
-                  MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL },
+                  MemException(e)  => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
                   MemValue(loaded) => {
                     let result : xlenbits =
                       match op {
@@ -347,7 +347,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                     match (wval) {
                       MemValue(true)  => { X(rd) = rval; RETIRE_SUCCESS },
                       MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
-                      MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
+                      MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
                     }
                   }
                 }
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index e60b96b5d..3b0817743 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -458,7 +458,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
             DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
           };
           match (eares) {
-            MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
+            MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
             MemValue(_) => {
               let rs2_val = F(rs2);
               match (width) {