From b5745a14b4e6e138d16671e84627d734f39e7f4e Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Thu, 7 May 2020 13:33:22 +0100
Subject: [PATCH] Do not add pointer primitive check for cprover internals

---
 src/analyses/goto_check.cpp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 8166485725f..52a6fc32e67 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
@@ -1187,12 +1188,23 @@ void goto_checkt::pointer_primitive_check(
   if(!enable_pointer_primitive_check)
     return;
 
+  if(expr.source_location().is_built_in())
+    return;
+
   const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok)
                           ? to_binary_expr(expr).lhs()
                           : to_unary_expr(expr).op();
 
   CHECK_RETURN(pointer.type().id() == ID_pointer);
 
+  if(pointer.id() == ID_symbol)
+  {
+    const auto &symbol_expr = to_symbol_expr(pointer);
+
+    if(has_prefix(id2string(symbol_expr.get_identifier()), CPROVER_PREFIX))
+      return;
+  }
+
   const auto size_of_expr_opt = size_of_expr(pointer.type().subtype(), ns);
 
   const exprt size = !size_of_expr_opt.has_value()