diff --git a/ir/attrs.cpp b/ir/attrs.cpp
index 661c67ceb..610957e0b 100644
--- a/ir/attrs.cpp
+++ b/ir/attrs.cpp
@@ -328,11 +328,6 @@ void ParamAttrs::merge(const ParamAttrs &other) {
   align            = max(align, other.align);
 }
 
-static expr merge(pair<AndExpr, expr> e) {
-  e.first.add(std::move(e.second));
-  return std::move(e.first)();
-}
-
 static expr
 encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
                uint64_t derefOrNullBytes, uint64_t align, bool nonnull,
diff --git a/ir/instr.cpp b/ir/instr.cpp
index 9ad35c5eb..abbf2c9b5 100644
--- a/ir/instr.cpp
+++ b/ir/instr.cpp
@@ -3164,10 +3164,18 @@ Assume::Assume(Value &cond, Kind kind)
 
 Assume::Assume(vector<Value *> &&args0, Kind kind)
     : Instr(Type::voidTy, "assume"), args(std::move(args0)), kind(kind) {
-  if (args.size() == 1)
-    assert(kind == AndNonPoison || kind == WellDefined || kind == NonNull);
-  else {
-    assert(kind == Align && args.size() == 2);
+  switch (kind) {
+    case AndNonPoison:
+    case WellDefined:
+    case NonNull:
+      assert(args.size() == 1);
+      break;
+
+    case Align:
+    case Dereferenceable:
+    case DereferenceableOrNull:
+      assert(args.size() == 2);
+      break;
   }
 }
 
@@ -3191,10 +3199,12 @@ void Assume::rauw(const Value &what, Value &with) {
 void Assume::print(ostream &os) const {
   const char *str = nullptr;
   switch (kind) {
-  case AndNonPoison: str = "assume "; break;
-  case WellDefined:  str = "assume_welldefined "; break;
-  case Align:        str = "assume_align "; break;
-  case NonNull:      str = "assume_nonnull "; break;
+  case AndNonPoison:          str = "assume "; break;
+  case WellDefined:           str = "assume_welldefined "; break;
+  case Align:                 str = "assume_align "; break;
+  case Dereferenceable:       str = "assume_dereferenceable "; break;
+  case DereferenceableOrNull: str = "assume_dereferenceable_or_null "; break;
+  case NonNull:               str = "assume_nonnull "; break;
   }
   os << str;
 
@@ -3226,11 +3236,19 @@ StateValue Assume::toSMT(State &s) const {
     s.addGuardableUB(Pointer(s.getMemory(), ptr).isAligned(align));
     break;
   }
+  case Dereferenceable:
+  case DereferenceableOrNull: {
+    const auto &vptr  = s.getAndAddPoisonUB(*args[0]).value;
+    const auto &bytes = s.getAndAddPoisonUB(*args[1]).value;
+    Pointer ptr(s.getMemory(), vptr);
+    expr nonnull = kind == DereferenceableOrNull ? !ptr.isNull() : false;
+    s.addUB(nonnull || merge(ptr.isDereferenceable(bytes, 1, false)));
+    break;
+  }
   case NonNull: {
     // assume(ptr)
-    const auto &vptr = s.getAndAddPoisonUB(*args[0]);
-    Pointer ptr(s.getMemory(), vptr.value);
-    s.addGuardableUB(!ptr.isNull());
+    const auto &ptr = s.getAndAddPoisonUB(*args[0]).value;
+    s.addGuardableUB(!Pointer(s.getMemory(), ptr).isNull());
     break;
   }
   }
@@ -3244,6 +3262,8 @@ expr Assume::getTypeConstraints(const Function &f) const {
   case AndNonPoison:
     return args[0]->getType().enforceIntType();
   case Align:
+  case Dereferenceable:
+  case DereferenceableOrNull:
     return args[0]->getType().enforcePtrType() &&
            args[1]->getType().enforceIntType();
   case NonNull:
diff --git a/ir/instr.h b/ir/instr.h
index 393a02495..e3e47c3f9 100644
--- a/ir/instr.h
+++ b/ir/instr.h
@@ -587,9 +587,11 @@ class Assume final : public Instr {
 public:
   enum Kind {
     AndNonPoison, /// cond should be non-poison and hold
-    WellDefined, /// cond only needs to be well defined (can be false)
-    Align,       /// args[0] satisfies alignment args[1]
-    NonNull      /// args[0] is a nonnull pointer
+    WellDefined,  /// cond only needs to be well defined (can be false)
+    Align,        /// args[0] satisfies alignment args[1]
+    Dereferenceable,       /// args[0] is dereferenceable at least args[1]
+    DereferenceableOrNull, /// args[0] is null or deref least args[1]
+    NonNull       /// args[0] is a nonnull pointer
   };
 
 private:
diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp
index ddb61d7c2..e1b019eb4 100644
--- a/llvm_util/llvm2alive.cpp
+++ b/llvm_util/llvm2alive.cpp
@@ -58,6 +58,14 @@ FpExceptionMode parse_exceptions(llvm::Instruction &i) {
   }
 }
 
+Value* get_ptr(Instr &i) {
+  for (auto *op : i.operands()) {
+    if (op->getType().isPtrType())
+      return op;
+  }
+  UNREACHABLE();
+}
+
 bool hit_limits;
 unsigned constexpr_idx;
 unsigned copy_idx;
@@ -1282,6 +1290,17 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
         BB->addInstr(make_unique<Assume>(*i, Assume::WellDefined));
         break;
 
+      case LLVMContext::MD_dereferenceable:
+      case LLVMContext::MD_dereferenceable_or_null: {
+        auto kind = ID == LLVMContext::MD_dereferenceable
+                      ? Assume::Dereferenceable : Assume::DereferenceableOrNull;
+        auto bytes = get_operand(
+          llvm::mdconst::extract<llvm::ConstantInt>(Node->getOperand(0)));
+        BB->addInstr(
+          make_unique<Assume>(vector<Value*>{get_ptr(*i), bytes}, kind));
+        break;
+      }
+
       // non-relevant for correctness
       case LLVMContext::MD_loop:
       case LLVMContext::MD_nosanitize:
diff --git a/smt/exprs.h b/smt/exprs.h
index 30d290205..0e2768249 100644
--- a/smt/exprs.h
+++ b/smt/exprs.h
@@ -212,3 +212,8 @@ class FunctionExpr {
 };
 
 }
+
+static inline smt::expr merge(std::pair<smt::AndExpr, smt::expr> e) {
+  e.first.add(std::move(e.second));
+  return std::move(e.first)();
+}
diff --git a/tests/alive-tv/memory/dereferenceable_metadata.srctgt.ll b/tests/alive-tv/memory/dereferenceable_metadata.srctgt.ll
new file mode 100644
index 000000000..d2c7bbb16
--- /dev/null
+++ b/tests/alive-tv/memory/dereferenceable_metadata.srctgt.ll
@@ -0,0 +1,11 @@
+define void @src(ptr %0) {
+  load <6 x i16>, ptr %0, align 16, !dereferenceable !0
+  ret void
+}
+
+define void @tgt(ptr %0) {
+  load i128, ptr %0, align 16
+  ret void
+}
+
+!0 = !{ i32 16 }