diff --git a/regression/cbmc/r_w_ok4/main.c b/regression/cbmc/r_w_ok4/main.c
new file mode 100644
index 00000000000..37cd21b8779
--- /dev/null
+++ b/regression/cbmc/r_w_ok4/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int A[1];
+
+  assert(__CPROVER_r_ok(A, sizeof(int)));
+}
diff --git a/regression/cbmc/r_w_ok4/test.desc b/regression/cbmc/r_w_ok4/test.desc
new file mode 100644
index 00000000000..278f468e130
--- /dev/null
+++ b/regression/cbmc/r_w_ok4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 87a7198933f..415e1f4e8ff 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2056,6 +2056,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt same_object_expr=
       same_object(expr.arguments()[0], expr.arguments()[1]);
     same_object_expr.add_source_location()=source_location;
@@ -2105,6 +2107,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()};
     same_object_expr.add_source_location()=source_location;
 
@@ -2119,6 +2123,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt buffer_size_expr("buffer_size", size_type());
     buffer_size_expr.operands()=expr.arguments();
     buffer_size_expr.add_source_location()=source_location;
@@ -2134,6 +2140,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     predicate_exprt is_zero_string_expr("is_zero_string");
     is_zero_string_expr.operands()=expr.arguments();
     is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
@@ -2150,6 +2158,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt zero_string_length_expr("zero_string_length", size_type());
     zero_string_length_expr.operands()=expr.arguments();
     zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
@@ -2166,6 +2176,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]);
     is_dynamic_object_expr.add_source_location() = source_location;
 
@@ -2180,6 +2192,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
     pointer_offset_expr.add_source_location()=source_location;
 
@@ -2194,6 +2208,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     unary_exprt object_size_expr(
       ID_object_size, expr.arguments()[0], size_type());
     object_size_expr.add_source_location() = source_location;
@@ -2209,6 +2225,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt pointer_object_expr = pointer_object(expr.arguments().front());
     pointer_object_expr.add_source_location() = source_location;
 
@@ -2218,8 +2236,6 @@ exprt c_typecheck_baset::do_special_functions(
           identifier=="__builtin_bswap32" ||
           identifier=="__builtin_bswap64")
   {
-    typecheck_function_call_arguments(expr);
-
     if(expr.arguments().size()!=1)
     {
       error().source_location = f_op.source_location();
@@ -2227,6 +2243,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // these are hard-wired to 8 bits according to the gcc manual
     bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
     bswap_expr.add_source_location()=source_location;
@@ -2235,8 +2253,6 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier=="__builtin_nontemporal_load")
   {
-    typecheck_function_call_arguments(expr);
-
     if(expr.arguments().size()!=1)
     {
       error().source_location = f_op.source_location();
@@ -2244,6 +2260,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // these return the subtype of the argument
     exprt &ptr_arg=expr.arguments().front();
 
@@ -2269,6 +2287,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // This gets 5 integers followed by a float or double.
     // The five integers are the return values for the cases
     // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
@@ -2315,6 +2335,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     isnan_exprt isnan_expr(expr.arguments().front());
     isnan_expr.add_source_location()=source_location;
 
@@ -2331,6 +2353,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     isfinite_exprt isfinite_expr(expr.arguments().front());
     isfinite_expr.add_source_location()=source_location;
 
@@ -2378,6 +2402,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     abs_exprt abs_expr(expr.arguments().front());
     abs_expr.add_source_location()=source_location;
 
@@ -2392,6 +2418,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
     malloc_expr.operands()=expr.arguments();
 
@@ -2407,6 +2435,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
 
     binary_predicate_exprt ok_expr(
@@ -2427,6 +2457,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     isinf_exprt isinf_expr(expr.arguments().front());
     isinf_expr.add_source_location()=source_location;
 
@@ -2441,6 +2473,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // returns 1 for +inf and -1 for -inf, and 0 otherwise
 
     const exprt &fp_value = expr.arguments().front();
@@ -2468,6 +2502,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     const exprt &fp_value = expr.arguments()[0];
 
     if(fp_value.type().id() != ID_floatbv)
@@ -2496,6 +2532,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     sign_exprt sign_expr(expr.arguments().front());
     sign_expr.add_source_location()=source_location;
 
@@ -2515,6 +2553,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     popcount_exprt popcount_expr(expr.arguments().front(), expr.type());
     popcount_expr.add_source_location()=source_location;
 
@@ -2529,6 +2569,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     equal_exprt equality_expr(
       expr.arguments().front(), expr.arguments().back());
     equality_expr.add_source_location()=source_location;
@@ -2557,6 +2599,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     return typecast_exprt(expr.arguments()[0], expr.type());
   }
   else if(identifier=="__builtin_object_size")
@@ -2572,6 +2616,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     make_constant(expr.arguments()[1]);
 
     mp_integer arg1;
@@ -2614,6 +2660,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt arg0 =
       typecast_exprt::conditional_cast(expr.arguments()[0], bool_typet());
     make_constant(arg0);
@@ -2634,6 +2682,9 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    // do not typecheck the argument - it is never evaluated, and thus side
+    // effects must not show up either
+
     // try to produce constant
     exprt tmp1=expr.arguments().front();
     simplify(tmp1, *this);
@@ -2671,6 +2722,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt object=expr.arguments()[0];
 
     // The value doesn't matter at all, we only care about the type.
@@ -2743,6 +2796,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt &ptr_arg=expr.arguments().front();
 
     if(ptr_arg.type().id()!=ID_pointer)