diff --git a/README.md b/README.md
index b4840670a..2eca7645b 100644
--- a/README.md
+++ b/README.md
@@ -76,7 +76,7 @@ Building and Running Translation Validation
 --------
 
 Alive2's `opt` and `clang` translation validation requires a build of LLVM with
-RTTI and exceptions turned on. The latest version of Alive2 is always intended
+RTTI and exceptions turned on. The latest version Of Alive2 is always intended
 to be built against the latest version of LLVM, using the main branch from
 the LLVM repo on Github.
 LLVM can be built in the following way.
@@ -107,6 +107,12 @@ cmake -GNinja -DCMAKE_PREFIX_PATH=~/llvm/build -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=R
 ninja
 ```
 
+Then to validate, and run all tests you can run:
+```
+ninja check
+```
+
+
 Translation validation of one or more LLVM passes transforming an IR file:
 ```
 ~/alive/build/alive-tv -passes=instcombine foo.ll
diff --git a/ir/memory.cpp b/ir/memory.cpp
index 879731074..f4f69cca3 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -1207,7 +1207,10 @@ static expr mk_store(expr mem, const expr &offset, const expr &val) {
 
 TypedByte Memory::raw_load(bool local, unsigned bid, const expr &offset) const {
   auto &block = (local ? local_block_val : non_local_block_val)[bid];
-  return { Byte(*this, ::raw_load(block.val, offset)), DataType(block.type) };
+  expr alive = isBlockAlive(expr::mkUInt(bid, Pointer::bitsShortBid()), local);
+  return { Byte(*this, mkIf_fold(alive, ::raw_load(block.val, offset),
+                                Byte::mkPoisonByte(*this)())),
+           DataType(block.type) };
 }
 
 vector<TypedByte>
@@ -1234,7 +1237,10 @@ Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &undef,
       assert(idx < blk_size);
       uint64_t max_idx = blk_size - bytes + idx;
       expr off = blk_offset + expr::mkUInt(idx, offset);
-      loaded[i].first.add(::raw_load(blk.val, off, max_idx), cond);
+      expr is_alive = isBlockAlive(expr::mkUInt(bid, Pointer::bitsShortBid()), local);
+      loaded[i].first.add(mkIf_fold(is_alive, ::raw_load(blk.val, off, max_idx),
+                                    poison),
+                          cond);
       loaded[i].second |= blk.type;
     }
     undef.insert(blk.undef.begin(), blk.undef.end());
diff --git a/ir/pointer.cpp b/ir/pointer.cpp
index 51bd9512f..2d5c26cfe 100644
--- a/ir/pointer.cpp
+++ b/ir/pointer.cpp
@@ -539,7 +539,9 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
   expr bytes = bytes0.zextOrTrunc(bits_for_offset);
 
   auto block_constraints = [&](const Pointer &p) {
-    expr ret = p.isBlockAlive();
+    expr ret = expr::mkIf(p.isStackAllocated(),
+                          (iswrite || is_asm) ? p.isBlockAlive() : true,
+                          p.isBlockAlive());
     if (iswrite)
       ret &= p.isWritable() && !p.isNoWrite();
     else if (!ignore_accessability)
diff --git a/tests/alive-tv/bugs/pr23599.srctgt.ll b/tests/alive-tv/bugs/pr23599.srctgt.ll
index 1aadf796e..1d1390de7 100644
--- a/tests/alive-tv/bugs/pr23599.srctgt.ll
+++ b/tests/alive-tv/bugs/pr23599.srctgt.ll
@@ -46,3 +46,5 @@ declare void @llvm.memset.p0i8.i64(ptr captures(none), i8, i64, i32, i1)
 declare void @llvm.memcpy.p0i8.p0i8.i64(ptr captures(none), ptr captures(none) readonly, i64, i32, i1)
 declare void @_Z5PrintRK12ether_header(ptr dereferenceable(12))
 declare void @llvm.lifetime.end(i64, ptr captures(none))
+
+; ERROR: Mismatch in memory
diff --git a/tests/alive-tv/calls/escape2.srctgt.ll b/tests/alive-tv/calls/escape2.srctgt.ll
index 8939cceb9..670326e16 100644
--- a/tests/alive-tv/calls/escape2.srctgt.ll
+++ b/tests/alive-tv/calls/escape2.srctgt.ll
@@ -1,8 +1,12 @@
 @glb = global ptr null
 declare ptr @f(ptr %p)
 
+declare void @llvm.lifetime.start(i64, ptr captures(none))
+declare void @llvm.lifetime.end(i64, ptr captures(none))
+
 define i8 @src() {
   %p = alloca i8
+  call void @llvm.lifetime.start(i64 1, ptr %p)
   store i8 1, ptr %p
 
   %q = load ptr, ptr @glb
@@ -10,16 +14,19 @@ define i8 @src() {
   store i8 2, ptr %q2
 
   %v = load i8, ptr %p
+  call void @llvm.lifetime.end(i64 1, ptr %p)
   ret i8 %v
 }
 
 define i8 @tgt() {
   %p = alloca i8
+  call void @llvm.lifetime.start(i64 1, ptr %p)
   store i8 1, ptr %p
 
   %q = load ptr, ptr @glb
   %q2 = call ptr @f(ptr %q) ; cannot be %p
   store i8 2, ptr %q2
 
+  call void @llvm.lifetime.end(i64 1, ptr %p)
   ret i8 1
 }
diff --git a/tests/alive-tv/calls/ptr-store.srctgt.ll b/tests/alive-tv/calls/ptr-store.srctgt.ll
index cc525ce4f..77805cdc9 100644
--- a/tests/alive-tv/calls/ptr-store.srctgt.ll
+++ b/tests/alive-tv/calls/ptr-store.srctgt.ll
@@ -1,14 +1,17 @@
 define void @src(ptr %0, i1 %1) {
   %3 = alloca i64, align 8
+  call void @llvm.lifetime.start(i64 8, ptr %3)
   store ptr null, ptr %0, align 8
   call void @fn()
   br i1 %1, label %4, label %5
 
 4:
+  call void @llvm.lifetime.end(i64 8, ptr %3)
   ret void
 
 5:
   store i64 0, ptr %3, align 8
+  call void @llvm.lifetime.end(i64 8, ptr %3)
   ret void
 }
 
@@ -19,3 +22,5 @@ define void @tgt(ptr %0, i1 %1) {
 }
 
 declare void @fn()
+declare void @llvm.lifetime.start(i64, ptr captures(none))
+declare void @llvm.lifetime.end(i64, ptr captures(none))
diff --git a/tests/alive-tv/lifetime-load-poison.srctgt.ll b/tests/alive-tv/lifetime-load-poison.srctgt.ll
new file mode 100644
index 000000000..c238352ef
--- /dev/null
+++ b/tests/alive-tv/lifetime-load-poison.srctgt.ll
@@ -0,0 +1,13 @@
+; ERROR: Source is more defined than target
+
+define i8 @src() {
+  %p = alloca i8
+  call void @llvm.lifetime.start.p0(ptr %p)
+  call void @llvm.lifetime.end.p0(ptr %p)
+  %v = load i8, ptr %p
+  ret i8 %v
+}
+
+define i8 @tgt() {
+  unreachable
+}