diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
index edbd9ade6..c539fe44f 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
@@ -215,6 +215,7 @@ import           Lang.Crucible.Simulator.SimError
 
 import           Lang.Crucible.LLVM.DataLayout
 import           Lang.Crucible.LLVM.Extension
+import           Lang.Crucible.LLVM.Extension.Safety
 import           Lang.Crucible.LLVM.Bytes
 import           Lang.Crucible.LLVM.MemType
 import           Lang.Crucible.LLVM.MemModel.Type
@@ -229,6 +230,7 @@ import           Lang.Crucible.LLVM.Types
 import           Lang.Crucible.Panic (panic)
 
 
+
 import           GHC.Stack
 
 ----------------------------------------------------------------------
@@ -971,22 +973,34 @@ isAllocatedAlignedPointer sym w alignment mutability ptr size mem =
 --
 --   The pointer to read from must be concrete and nonnull.  The contents
 --   of the string may be symbolic; HOWEVER, this function will not terminate
---   unless there it eventually reaches a concete null-terminator.
+--   until it eventually reaches a concete null-terminator or a load error.
 strLen :: forall sym wptr.
   (IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym) =>
   sym ->
   MemImpl sym      {- ^ memory to read from        -} ->
   LLVMPtr sym wptr {- ^ pointer to string value    -} ->
   IO (SymBV sym wptr)
-strLen sym mem = go 0
+strLen sym mem = go 0 (truePred sym)
   where
-  go !n p =
-    do v <- doLoad sym mem p (bitvectorType 1) (LLVMPointerRepr (knownNat @8)) noAlignment
-       test <- bvIsNonzero sym =<< projectLLVM_bv sym v
-       iteM bvIte sym
-            test
-            (go (n+1) =<< doPtrAddOffset sym mem p =<< bvLit sym PtrWidth 1)
-            (bvLit sym PtrWidth n)
+  go !n cond p =
+    loadRaw sym mem p (bitvectorType 1) noAlignment >>= \case
+      Partial.Err e ->
+        do ast <- impliesPred sym cond (falsePred sym)
+           let msg = show (ppMemoryLoadError e)
+           assert sym ast $ AssertFailureSimError "Error during memory load: strlen" msg
+           bvLit sym PtrWidth (maxUnsigned PtrWidth) -- bogus value, but have to return something...
+      Partial.NoErr loadok llvmval ->
+        do ast <- impliesPred sym cond loadok
+           assert sym ast $ AssertFailureSimError "Error during memory load: strlen" ""
+           v <- unpackMemValue sym (LLVMPointerRepr (knownNat @8)) llvmval
+           test <- bvIsNonzero sym =<< projectLLVM_bv sym v
+           iteM bvIte sym
+             test
+             (do cond' <- andPred sym cond test
+                 p'    <- doPtrAddOffset sym mem p =<< bvLit sym PtrWidth 1
+                 go (n+1) cond' p')
+             (bvLit sym PtrWidth n)
+
 
 -- | Load a null-terminated string from the memory.
 --
diff --git a/crux-llvm/test-data/golden/strlen_test.c b/crux-llvm/test-data/golden/strlen_test.c
new file mode 100644
index 000000000..e14d935ce
--- /dev/null
+++ b/crux-llvm/test-data/golden/strlen_test.c
@@ -0,0 +1,23 @@
+#include <stdlib.h>
+#include <string.h>
+
+#include "crucible.h"
+
+#define MAX 10
+
+char* mkstr() {
+  char* x = malloc(MAX);
+  for( int i=0; i<MAX; i++ ) {
+    x[i] = crucible_int8_t( "x" );
+  }
+
+  assuming( x[MAX-1] == 0 );
+
+  return x;
+}
+
+int main() {
+  char *str = mkstr();
+  size_t sz = strlen(str);
+  check( sz < MAX );
+}
diff --git a/crux-llvm/test-data/golden/strlen_test.good b/crux-llvm/test-data/golden/strlen_test.good
new file mode 100644
index 000000000..9c7ea10d9
--- /dev/null
+++ b/crux-llvm/test-data/golden/strlen_test.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.