diff --git a/intTests/test1945/Makefile b/intTests/test1945/Makefile
new file mode 100644
index 0000000000..ebf9cc47cc
--- /dev/null
+++ b/intTests/test1945/Makefile
@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -frecord-command-line -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc
diff --git a/intTests/test1945/test.bc b/intTests/test1945/test.bc
new file mode 100644
index 0000000000..f30cc928b2
Binary files /dev/null and b/intTests/test1945/test.bc differ
diff --git a/intTests/test1945/test.c b/intTests/test1945/test.c
new file mode 100644
index 0000000000..32ff9ad7fa
--- /dev/null
+++ b/intTests/test1945/test.c
@@ -0,0 +1,3 @@
+#include <stdint.h>
+
+void test(uint8_t *x) {}
diff --git a/intTests/test1945/test.saw b/intTests/test1945/test.saw
new file mode 100644
index 0000000000..2475cf87d8
--- /dev/null
+++ b/intTests/test1945/test.saw
@@ -0,0 +1,17 @@
+// Test a use of `llvm_conditional_points_to` where the value that the pointer
+// points to will fail to match against the right-hand side value unless the
+// condition is properly incorporated into the path condition. This serves as
+// a regression test for https://github.com/GaloisInc/saw-script/issues/1945.
+
+let test_spec = do {
+  p <- llvm_alloc (llvm_int 8);
+  x <- llvm_fresh_var "x" (llvm_int 8);
+  llvm_points_to p (llvm_term x);
+
+  llvm_execute_func [p];
+
+  llvm_conditional_points_to {{ x == 1 }} p (llvm_term {{ 1 : [8] }});
+};
+
+m <- llvm_load_module "test.bc";
+llvm_verify m "test" [] false test_spec z3;
diff --git a/intTests/test1945/test.sh b/intTests/test1945/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test1945/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 1a0d1ed882..8174385b8a 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1410,14 +1410,28 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
             let badLoadSummary = summarizeBadLoad cc memTy prepost ptr
             case res of
               Crucible.NoErr pred_ res_val -> do
-                pred_' <- case maybe_cond of
-                  Just cond -> do
-                    cond' <- instantiateExtResolveSAWPred sc cc (ttTerm cond)
-                    liftIO $ W4.impliesPred sym cond' pred_
-                  Nothing -> return pred_
+                -- If dealing with an `llvm_conditional_points_to` statement,
+                -- convert the condition to a `Pred`. If dealing with an
+                -- ordinary `llvm_points_to` statement, this condition will
+                -- simply be `True`.
+                cond' <- case maybe_cond of
+                  Just cond ->
+                    instantiateExtResolveSAWPred sc cc (ttTerm cond)
+                  Nothing ->
+                    pure $ W4.truePred sym
+                -- Next, construct an implication involving the condition and
+                -- assert it.
+                pred_' <- liftIO $ W4.impliesPred sym cond' pred_
                 addAssert pred_' md $ Crucible.SimError loc $
                   Crucible.AssertFailureSimError (show $ PP.vcat badLoadSummary) ""
-                pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val'
+
+                -- Finally, match the value that the pointer points to against
+                -- the right-hand side value in the points_to statement. Make
+                -- sure to execute this match with an extended path condition
+                -- that takes the condition above into account. See also
+                -- Note [oeConditionalPred] in SAWScript.Crucible.Common.Override.
+                withConditionalPred cond' $
+                  pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val'
               _ -> do
                 pure $ Just $ describeConcreteMemoryLoadFailure mem badLoadSummary ptr