diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md
index c0aaf688255..40f9c10eede 100644
--- a/doc/cprover-manual/properties.md
+++ b/doc/cprover-manual/properties.md
@@ -122,6 +122,7 @@ The goto-instrument program supports these checks:
 | `--bounds-check`             |  add array bounds checks                             |
 | `--div-by-zero-check`        |  add division by zero checks                         |
 | `--pointer-check`            |  add pointer checks                                  |
+| `--pointer-primitive-check`  |  add pointer primitive checks                        |
 | `--signed-overflow-check`    |  add arithmetic over- and underflow checks           |
 | `--unsigned-overflow-check`  |  add arithmetic over- and underflow checks           |
 | `--undefined-shift-check`    |  add range checks for shift distances                |
diff --git a/regression/cbmc/pragma_cprover3/main.c b/regression/cbmc/pragma_cprover3/main.c
new file mode 100644
index 00000000000..f4dab2f722c
--- /dev/null
+++ b/regression/cbmc/pragma_cprover3/main.c
@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *p = malloc(sizeof(*p));
+  char *q;
+
+#pragma CPROVER check push
+#pragma CPROVER check disable "pointer-primitive"
+  // do not generate checks for the following statements
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+#pragma CPROVER check pop
+
+  // generate check and fail on the following statements
+  if(__CPROVER_same_object(p, q))
+  {
+  }
+}
diff --git a/regression/cbmc/pragma_cprover3/test.desc b/regression/cbmc/pragma_cprover3/test.desc
new file mode 100644
index 00000000000..a6ef5f1dbb8
--- /dev/null
+++ b/regression/cbmc/pragma_cprover3/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--pointer-primitive-check
+^main.c function main$
+^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
+^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 92de9458112..295988fdf6f 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -234,9 +234,10 @@ CPROVER_PREFIX  "__CPROVER_"
 
 arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero")
 enum_check      "enum-range"
+pointer_primitive "pointer-primitive"
 memory_check    ("bounds"|"pointer"|"memory_leak")
 overflow_check  ("signed"|"unsigned"|"pointer"|"float")"-overflow"
-named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check})["]
+named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check}|{pointer_primitive})["]
 
 %x GRAMMAR
 %x COMMENT1