diff --git a/regression/contracts/assigns_enforce_structs_07/main.c b/regression/contracts/assigns_enforce_structs_07/main.c
index 4651df53afa..f3ae51d8bc1 100644
--- a/regression/contracts/assigns_enforce_structs_07/main.c
+++ b/regression/contracts/assigns_enforce_structs_07/main.c
@@ -25,9 +25,12 @@ void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf))
 
 int main()
 {
-  struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
+  struct pair *p = malloc(sizeof(*p));
   f1(p);
+
   struct pair_of_pairs *pp = malloc(sizeof(*pp));
+  if(pp)
+    pp->p = malloc(sizeof(*(pp->p)));
   f2(pp);
 
   return 0;
diff --git a/regression/contracts/assigns_enforce_structs_07/test.desc b/regression/contracts/assigns_enforce_structs_07/test.desc
index 35858e11474..6e1780e42df 100644
--- a/regression/contracts/assigns_enforce_structs_07/test.desc
+++ b/regression/contracts/assigns_enforce_structs_07/test.desc
@@ -1,17 +1,16 @@
-KNOWNBUG
+CORE
 main.c
---enforce-all-contracts _ --pointer-check
+--enforce-all-contracts _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$
 ^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
-^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$
 ^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
 Checks whether CBMC properly evaluates write set of members
 from invalid objects. In this case, they are not writable.
-
-Bug: We need to check the validity of each dereference
-when accessing struct members.
diff --git a/regression/contracts/assigns_replace_07/main.c b/regression/contracts/assigns_replace_07/main.c
index 16bf52c0ab8..afa44dc1bf8 100644
--- a/regression/contracts/assigns_replace_07/main.c
+++ b/regression/contracts/assigns_replace_07/main.c
@@ -2,24 +2,23 @@
 #include <stdint.h>
 #include <stdlib.h>
 
-struct pair
+struct test
 {
-  uint8_t *buf;
-  size_t size;
+  uint8_t buf[8];
 };
 
-void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
-  __CPROVER_ensures(p->buf[0] == 0)
+void f1(struct test *p) __CPROVER_assigns(p->buf)
+  __CPROVER_ensures((p == NULL) || p->buf[0] == 0)
 {
-  p->buf[0] = 0;
+  if(p != NULL)
+    p->buf[0] = 0;
 }
 
 int main()
 {
-  struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
+  struct test *p = malloc(sizeof(*p));
+  uint8_t buf_1 = (p == NULL) ? 0 : p->buf[1];
   f1(p);
-  // clang-format off
-  assert(p != NULL ==> p->buf[0] == 0);
-  // clang-format on
-  return 0;
+  assert(p == NULL || p->buf[0] == 0);
+  assert(p == NULL || p->buf[1] == buf_1);
 }
diff --git a/regression/contracts/assigns_replace_07/test.desc b/regression/contracts/assigns_replace_07/test.desc
index d7c4d1a0492..6d734f8cb82 100644
--- a/regression/contracts/assigns_replace_07/test.desc
+++ b/regression/contracts/assigns_replace_07/test.desc
@@ -1,12 +1,13 @@
 CORE
 main.c
---replace-all-calls-with-contracts _ --pointer-check
+--replace-all-calls-with-contracts _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
-^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=> p->buf\[0\] \=\= 0: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[0\] == 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[1\] == buf_1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
-Checks whether CBMC properly evaluates write set of members
-from invalid objects. In this case, they are not writable.
+Checks whether CBMC properly evaluates write set of members from invalid objects.
+Functions are not expected to write to invalid locations; CBMC flags such writes.
+For contract checking, we ignore invalid targets in assigns clauses and assignment LHS.
diff --git a/regression/contracts/invar_loop-entry_check/main.c b/regression/contracts/invar_loop-entry_check/main.c
index c89606e0886..5e8b4bb5a00 100644
--- a/regression/contracts/invar_loop-entry_check/main.c
+++ b/regression/contracts/invar_loop-entry_check/main.c
@@ -33,17 +33,17 @@ void main()
   assert(x2 == z2);
 
   int y3;
-  s *s1, *s2;
+  s s0, s1, *s2 = &s0;
   s2->n = malloc(sizeof(int));
-  s1->n = s2->n;
+  s1.n = s2->n;
 
   while(y3 > 0)
-    __CPROVER_loop_invariant(s1->n == __CPROVER_loop_entry(s1->n))
+    __CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n))
     {
       --y3;
-      s1->n = s1->n + 1;
-      s1->n = s1->n - 1;
+      s0.n = s0.n + 1;
+      s2->n = s2->n - 1;
     }
 
-  assert(*(s1->n) == *(s2->n));
+  assert(*(s1.n) == *(s2->n));
 }
diff --git a/regression/contracts/invar_loop-entry_check/test.desc b/regression/contracts/invar_loop-entry_check/test.desc
index e563175416b..8278230c49e 100644
--- a/regression/contracts/invar_loop-entry_check/test.desc
+++ b/regression/contracts/invar_loop-entry_check/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
@@ -11,7 +11,7 @@ main.c
 ^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
 ^\[main.5\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.3\] .* assertion \*\(s1->n\) == \*\(s2->n\): SUCCESS$
+^\[main.assertion.3\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index aa54b13f969..53ed886c9f1 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -17,8 +17,9 @@ SRC = accelerate/accelerate.cpp \
       branch.cpp \
       call_sequences.cpp \
       contracts/assigns.cpp \
-      contracts/memory_predicates.cpp \
       contracts/contracts.cpp \
+      contracts/memory_predicates.cpp \
+      contracts/utils.cpp \
       concurrency.cpp \
       count_eloc.cpp \
       cover.cpp \
diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index 0cd7db453a0..7c99ade7c77 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/src/goto-instrument/contracts/assigns.cpp
@@ -15,10 +15,13 @@ Date: July 2021
 
 #include <goto-instrument/havoc_utils.h>
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
+#include <langapi/language_util.h>
+
+#include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
+#include "utils.h"
+
 assigns_clauset::targett::targett(
   const assigns_clauset &parent,
   const exprt &expr)
@@ -43,27 +46,16 @@ exprt assigns_clauset::targett::normalize(const exprt &expr)
 exprt assigns_clauset::targett::generate_containment_check(
   const address_of_exprt &lhs_address) const
 {
-  exprt::operandst address_validity;
-  exprt::operandst containment_check;
-
-  // __CPROVER_w_ok(target, sizeof(target))
-  address_validity.push_back(w_ok_exprt(
-    address,
-    size_of_expr(dereference_exprt(address).type(), parent.ns).value()));
+  const auto address_validity = and_exprt{
+    all_dereferences_are_valid(dereference_exprt{address}, parent.ns),
+    all_dereferences_are_valid(dereference_exprt{lhs_address}, parent.ns)};
 
-  // __CPROVER_w_ok(lhs, sizeof(lhs))
-  address_validity.push_back(w_ok_exprt(
-    lhs_address,
-    size_of_expr(dereference_exprt(lhs_address).type(), parent.ns).value()));
-
-  // __CPROVER_same_object(lhs, target)
+  exprt::operandst containment_check;
   containment_check.push_back(same_object(lhs_address, address));
 
   // If assigns target was a dereference, comparing objects is enough
-  // and the resulting condition will be
-  // __CPROVER_w_ok(target, sizeof(target))
-  // && __CPROVER_w_ok(lhs, sizeof(lhs))
-  // ==> __CPROVER_same_object(lhs, target)
+  // and the resulting condition will be:
+  // VALID(self) && VALID(lhs) ==> __CPROVER_same_object(lhs, self)
   if(id != ID_dereference)
   {
     const auto lhs_offset = pointer_offset(lhs_address);
@@ -86,19 +78,17 @@ exprt assigns_clauset::targett::generate_containment_check(
       own_offset);
 
     // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
-    // (sizeof(target) + __CPROVER_offset(target))
+    // (sizeof(self) + __CPROVER_offset(self))
     containment_check.push_back(
       binary_relation_exprt(lhs_region, ID_le, own_region));
   }
 
-  // __CPROVER_w_ok(target, sizeof(target))
-  // && __CPROVER_w_ok(lhs, sizeof(lhs))
-  // ==> __CPROVER_same_object(lhs, target)
-  //     && __CPROVER_offset(lhs) >= __CPROVER_offset(target)
-  //     && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
-  //        (sizeof(target) + __CPROVER_offset(target))
-  return binary_relation_exprt(
-    conjunction(address_validity), ID_implies, conjunction(containment_check));
+  // VALID(self) && VALID(lhs)
+  // ==> __CPROVER_same_object(lhs, self)
+  //  && __CPROVER_offset(lhs) >= __CPROVER_offset(self)
+  //  && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
+  //        (sizeof(self) + __CPROVER_offset(self))
+  return or_exprt{not_exprt{address_validity}, conjunction(containment_check)};
 }
 
 assigns_clauset::assigns_clauset(
@@ -147,12 +137,13 @@ goto_programt assigns_clauset::generate_havoc_code() const
   modifiest modifies;
   for(const auto &target : global_write_set)
     modifies.insert(target.address.object());
-
   for(const auto &target : local_write_set)
     modifies.insert(target.address.object());
 
   goto_programt havoc_statements;
-  append_havoc_code(location, modifies, havoc_statements);
+  havoc_if_validt havoc_gen(modifies, ns);
+  havoc_gen.append_full_havoc_code(location, havoc_statements);
+
   return havoc_statements;
 }
 
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index 1071ce8fb79..adfead3f6b6 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -14,9 +14,12 @@ Date: July 2021
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
 
-#include "contracts.h"
+#include <unordered_set>
 
-#include <util/pointer_offset_size.h>
+#include <goto-programs/goto_model.h>
+
+#include <util/message.h>
+#include <util/pointer_expr.h>
 
 /// \brief A class for representing assigns clauses in code contracts
 class assigns_clauset
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 16aedcdfb23..b99c2412dd7 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -24,6 +24,8 @@ Date: February 2016
 
 #include <goto-programs/remove_skip.h>
 
+#include <langapi/language_util.h>
+
 #include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
@@ -31,66 +33,12 @@ Date: February 2016
 #include <util/mathematical_types.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
 
 #include "assigns.h"
 #include "memory_predicates.h"
-
-// Create a lexicographic less-than relation between two tuples of variables.
-// This is used in the implementation of multidimensional decreases clauses.
-static exprt create_lexicographic_less_than(
-  const std::vector<symbol_exprt> &lhs,
-  const std::vector<symbol_exprt> &rhs)
-{
-  PRECONDITION(lhs.size() == rhs.size());
-
-  if(lhs.empty())
-  {
-    return false_exprt();
-  }
-
-  // Store conjunctions of equalities.
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
-  // s1 == l1 && s2 == l2 && s3 == l3>.
-  // In fact, the last element is unnecessary, so we do not create it.
-  exprt::operandst equality_conjunctions(lhs.size());
-  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
-  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
-  {
-    binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
-    equality_conjunctions[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_equality);
-  }
-
-  // Store inequalities between the i-th components of the input vectors
-  // (i.e. lhs and rhs).
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
-  // s2 == l2 && s3 < l3>.
-  exprt::operandst lexicographic_individual_comparisons(lhs.size());
-  lexicographic_individual_comparisons[0] =
-    binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
-  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
-  {
-    binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
-    lexicographic_individual_comparisons[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_less_than);
-  }
-  return disjunction(lexicographic_individual_comparisons);
-}
-
-static void insert_before_swap_and_advance(
-  goto_programt &program,
-  goto_programt::targett &target,
-  goto_programt &payload)
-{
-  const auto offset = payload.instructions.size();
-  program.insert_before_swap(target, payload);
-  std::advance(target, offset);
-}
+#include "utils.h"
 
 void code_contractst::check_apply_loop_contracts(
   goto_functionst::goto_functiont &goto_function,
@@ -203,7 +151,8 @@ void code_contractst::check_apply_loop_contracts(
   }
 
   // havoc the variables that may be modified
-  append_havoc_code(loop_head->source_location, modifies, havoc_code);
+  havoc_if_validt havoc_gen(modifies, ns);
+  havoc_gen.append_full_havoc_code(loop_head->source_location, havoc_code);
 
   // Generate: assume(invariant) just after havocing
   // We use a block scope to create a temporary assumption,
@@ -289,7 +238,8 @@ void code_contractst::check_apply_loop_contracts(
     // after the loop is smaller than the value before the loop.
     // Here, we use the lexicographic order.
     code_assertt monotonic_decreasing_assertion{
-      create_lexicographic_less_than(new_decreases_vars, old_decreases_vars)};
+      generate_lexicographic_less_than_check(
+        new_decreases_vars, old_decreases_vars)};
     monotonic_decreasing_assertion.add_source_location() =
       loop_head->source_location;
     converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode);
@@ -418,6 +368,11 @@ void code_contractst::replace_history_parameter(
 
       if(it == parameter2history.end())
       {
+        // 0. Create a skip target to jump to, if the parameter is invalid
+        goto_programt skip_program;
+        const auto skip_target =
+          skip_program.add(goto_programt::make_skip(location));
+
         // 1. Create a temporary symbol expression that represents the
         // history variable
         symbol_exprt tmp_symbol =
@@ -428,14 +383,23 @@ void code_contractst::replace_history_parameter(
         parameter2history[parameter] = tmp_symbol;
 
         // 3. Add the required instructions to the instructions list
-        // 3.1 Declare the newly created temporary variable
+        // 3.1. Declare the newly created temporary variable
         history.add(goto_programt::make_decl(tmp_symbol, location));
 
-        // 3.2 Add an assignment such that the value pointed to by the new
+        // 3.2. Skip storing the history if the expression is invalid
+        history.add(goto_programt::make_goto(
+          skip_target,
+          not_exprt{all_dereferences_are_valid(parameter, ns)},
+          location));
+
+        // 3.3. Add an assignment such that the value pointed to by the new
         // temporary variable is equal to the value of the corresponding
         // parameter
         history.add(
           goto_programt::make_assignment(tmp_symbol, parameter, location));
+
+        // 3.4. Add a skip target
+        history.destructive_append(skip_program);
       }
 
       expr = parameter2history[parameter];
diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h
index 4f0fd8fc947..2372a36a7d7 100644
--- a/src/goto-instrument/contracts/contracts.h
+++ b/src/goto-instrument/contracts/contracts.h
@@ -25,8 +25,6 @@ Date: February 2016
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
-#include <langapi/language_util.h>
-
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
new file mode 100644
index 00000000000..4f4d772988a
--- /dev/null
+++ b/src/goto-instrument/contracts/utils.cpp
@@ -0,0 +1,123 @@
+/*******************************************************************\
+
+Module: Utility functions for code contracts.
+
+Author: Saswat Padhi, saspadhi@amazon.com
+
+Date: September 2021
+
+\*******************************************************************/
+
+#include "utils.h"
+
+#include <util/pointer_expr.h>
+#include <util/pointer_predicates.h>
+
+static void append_safe_havoc_code_for_expr(
+  const source_locationt location,
+  const namespacet &ns,
+  const exprt &expr,
+  goto_programt &dest,
+  const std::function<void()> &havoc_code_impl)
+{
+  goto_programt skip_program;
+  const auto skip_target = skip_program.add(goto_programt::make_skip(location));
+
+  // skip havocing only if all pointer derefs in the expression are valid
+  // (to avoid spurious pointer deref errors)
+  dest.add(goto_programt::make_goto(
+    skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location));
+
+  havoc_code_impl();
+
+  // add the final skip target
+  dest.destructive_append(skip_program);
+}
+
+void havoc_if_validt::append_object_havoc_code_for_expr(
+  const source_locationt location,
+  const exprt &expr,
+  goto_programt &dest) const
+{
+  append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
+    havoc_utilst::append_object_havoc_code_for_expr(location, expr, dest);
+  });
+}
+
+void havoc_if_validt::append_scalar_havoc_code_for_expr(
+  const source_locationt location,
+  const exprt &expr,
+  goto_programt &dest) const
+{
+  append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
+    havoc_utilst::append_scalar_havoc_code_for_expr(location, expr, dest);
+  });
+}
+
+exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
+{
+  exprt::operandst validity_checks;
+
+  if(expr.id() == ID_dereference)
+    validity_checks.push_back(
+      good_pointer_def(to_dereference_expr(expr).pointer(), ns));
+
+  for(const auto &op : expr.operands())
+    validity_checks.push_back(all_dereferences_are_valid(op, ns));
+
+  return conjunction(validity_checks);
+}
+
+exprt generate_lexicographic_less_than_check(
+  const std::vector<symbol_exprt> &lhs,
+  const std::vector<symbol_exprt> &rhs)
+{
+  PRECONDITION(lhs.size() == rhs.size());
+
+  if(lhs.empty())
+  {
+    return false_exprt();
+  }
+
+  // Store conjunctions of equalities.
+  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
+  // l2, l3>.
+  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
+  // s1 == l1 && s2 == l2 && s3 == l3>.
+  // In fact, the last element is unnecessary, so we do not create it.
+  exprt::operandst equality_conjunctions(lhs.size());
+  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
+  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
+  {
+    binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
+    equality_conjunctions[i] =
+      and_exprt(equality_conjunctions[i - 1], component_i_equality);
+  }
+
+  // Store inequalities between the i-th components of the input vectors
+  // (i.e. lhs and rhs).
+  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
+  // l2, l3>.
+  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
+  // s2 == l2 && s3 < l3>.
+  exprt::operandst lexicographic_individual_comparisons(lhs.size());
+  lexicographic_individual_comparisons[0] =
+    binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
+  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
+  {
+    binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
+    lexicographic_individual_comparisons[i] =
+      and_exprt(equality_conjunctions[i - 1], component_i_less_than);
+  }
+  return disjunction(lexicographic_individual_comparisons);
+}
+
+void insert_before_swap_and_advance(
+  goto_programt &destination,
+  goto_programt::targett &target,
+  goto_programt &payload)
+{
+  const auto offset = payload.instructions.size();
+  destination.insert_before_swap(target, payload);
+  std::advance(target, offset);
+}
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
new file mode 100644
index 00000000000..c82de0f0ce5
--- /dev/null
+++ b/src/goto-instrument/contracts/utils.h
@@ -0,0 +1,92 @@
+/*******************************************************************\
+
+Module: Utility functions for code contracts.
+
+Author: Saswat Padhi, saspadhi@amazon.com
+
+Date: September 2021
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
+
+#include <vector>
+
+#include <goto-instrument/havoc_utils.h>
+
+#include <goto-programs/goto_model.h>
+
+/// \brief A class that overrides the low-level havocing functions in the base
+///        utility class, to havoc only when expressions point to valid memory,
+///        i.e. if all dereferences within an expression are valid
+class havoc_if_validt : public havoc_utilst
+{
+public:
+  havoc_if_validt(const modifiest &mod, const namespacet &ns)
+    : havoc_utilst(mod), ns(ns)
+  {
+  }
+
+  void append_object_havoc_code_for_expr(
+    const source_locationt location,
+    const exprt &expr,
+    goto_programt &dest) const override;
+
+  void append_scalar_havoc_code_for_expr(
+    const source_locationt location,
+    const exprt &expr,
+    goto_programt &dest) const override;
+
+protected:
+  const namespacet &ns;
+};
+
+/// \brief Generate a validity check over all dereferences in an expression
+///
+/// This function generates a formula:
+///
+///   good_pointer_def(pexpr_1, ns) &&
+///   good_pointer_def(pexpr_2, n2) &&
+///   ...
+///
+/// over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ...
+/// found in the AST of `expr`.
+///
+/// \param expr The expression that contains dereferences to be validated
+/// \param ns The namespace that defines all symbols appearing in `expr`
+/// \return A conjunctive expression that checks validity of all pointers
+///         that are dereferenced within `expr`
+exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns);
+
+/// \brief Generate a lexicographic less-than comparison over ordered tuples
+///
+/// This function creates an expression representing a lexicographic less-than
+/// comparison, lhs < rhs, between two ordered tuples of variables.
+/// This is used in instrumentation of decreases clauses.
+///
+/// \param lhs A vector of variables representing the LHS of the comparison
+/// \param rhs A vector of variables representing the RHS of the comparison
+/// \return A lexicographic less-than comparison expression: LHS < RHS
+exprt generate_lexicographic_less_than_check(
+  const std::vector<symbol_exprt> &lhs,
+  const std::vector<symbol_exprt> &rhs);
+
+/// \brief Insert a goto program before a target instruction iterator
+///        and advance the iterator.
+///
+/// This function inserts all instruction from a goto program `payload` into a
+/// destination program `destination` immediately before a specified instruction
+/// iterator `target`.
+/// After insertion, `target` is advanced by the size of the `payload`,
+/// and `payload` is destroyed.
+///
+/// \param destination The destination program for inserting the `payload`
+/// \param target The instruction iterator at which to insert the `payload`
+/// \param payload The goto program to be inserted into the `destination`
+void insert_before_swap_and_advance(
+  goto_programt &destination,
+  goto_programt::targett &target,
+  goto_programt &payload);
+
+#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp
index a62a0689d71..18c792a3eae 100644
--- a/src/goto-instrument/havoc_loops.cpp
+++ b/src/goto-instrument/havoc_loops.cpp
@@ -68,7 +68,8 @@ void havoc_loopst::havoc_loop(
 
   // build the havocking code
   goto_programt havoc_code;
-  append_havoc_code(loop_head->source_location, modifies, havoc_code);
+  havoc_utilst havoc_gen(modifies);
+  havoc_gen.append_full_havoc_code(loop_head->source_location, havoc_code);
 
   // Now havoc at the loop head. Use insert_swap to
   // preserve jumps to loop head.
diff --git a/src/goto-instrument/havoc_utils.cpp b/src/goto-instrument/havoc_utils.cpp
index 7b4066ed49f..c1451c4668a 100644
--- a/src/goto-instrument/havoc_utils.cpp
+++ b/src/goto-instrument/havoc_utils.cpp
@@ -17,78 +17,49 @@ Date: July 2021
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
 
-void append_safe_havoc_code_for_expr(
-  const source_locationt source_location,
-  const exprt &expr,
-  goto_programt &dest,
-  const std::function<void()> &havoc_code_impl)
+void havoc_utilst::append_full_havoc_code(
+  const source_locationt location,
+  goto_programt &dest) const
 {
-  goto_programt skip_program;
-  const auto skip_target =
-    skip_program.add(goto_programt::make_skip(source_location));
-
-  // for deref expressions, check for validity of underlying pointer,
-  // and skip havocing if invalid (to avoid spurious pointer deref errors)
-  if(expr.id() == ID_dereference)
-  {
-    const auto condition = not_exprt(w_ok_exprt(
-      to_dereference_expr(expr).pointer(),
-      from_integer(0, unsigned_int_type())));
-    dest.add(goto_programt::make_goto(skip_target, condition, source_location));
-  }
-
-  havoc_code_impl();
-
-  // for deref expressions, add the final skip target
-  if(expr.id() == ID_dereference)
-    dest.destructive_append(skip_program);
+  for(const auto &expr : modifies)
+    append_havoc_code_for_expr(location, expr, dest);
 }
 
-void append_object_havoc_code_for_expr(
-  const source_locationt source_location,
+void havoc_utilst::append_havoc_code_for_expr(
+  const source_locationt location,
   const exprt &expr,
-  goto_programt &dest)
+  goto_programt &dest) const
 {
-  append_safe_havoc_code_for_expr(source_location, expr, dest, [&]() {
-    codet havoc(ID_havoc_object);
-    havoc.add_source_location() = source_location;
-    havoc.add_to_operands(expr);
-    dest.add(goto_programt::make_other(havoc, source_location));
-  });
+  if(expr.id() == ID_index || expr.id() == ID_dereference)
+  {
+    address_of_exprt address_of_expr(expr);
+    if(!is_constant(address_of_expr))
+    {
+      append_object_havoc_code_for_expr(location, address_of_expr, dest);
+      return;
+    }
+  }
+  append_scalar_havoc_code_for_expr(location, expr, dest);
 }
 
-void append_scalar_havoc_code_for_expr(
-  const source_locationt source_location,
+void havoc_utilst::append_object_havoc_code_for_expr(
+  const source_locationt location,
   const exprt &expr,
-  goto_programt &dest)
+  goto_programt &dest) const
 {
-  append_safe_havoc_code_for_expr(source_location, expr, dest, [&]() {
-    side_effect_expr_nondett rhs(expr.type(), source_location);
-    goto_programt::targett t = dest.add(
-      goto_programt::make_assignment(expr, std::move(rhs), source_location));
-    t->code_nonconst().add_source_location() = source_location;
-  });
+  codet havoc(ID_havoc_object);
+  havoc.add_source_location() = location;
+  havoc.add_to_operands(expr);
+  dest.add(goto_programt::make_other(havoc, location));
 }
 
-void append_havoc_code(
-  const source_locationt source_location,
-  const modifiest &modifies,
-  goto_programt &dest)
+void havoc_utilst::append_scalar_havoc_code_for_expr(
+  const source_locationt location,
+  const exprt &expr,
+  goto_programt &dest) const
 {
-  havoc_utils_is_constantt is_constant(modifies);
-  for(const auto &expr : modifies)
-  {
-    if(expr.id() == ID_index || expr.id() == ID_dereference)
-    {
-      address_of_exprt address_of_expr(expr);
-      if(!is_constant(address_of_expr))
-      {
-        append_object_havoc_code_for_expr(
-          source_location, address_of_expr, dest);
-        continue;
-      }
-    }
-
-    append_scalar_havoc_code_for_expr(source_location, expr, dest);
-  }
+  side_effect_expr_nondett rhs(expr.type(), location);
+  goto_programt::targett t =
+    dest.add(goto_programt::make_assignment(expr, std::move(rhs), location));
+  t->code_nonconst().add_source_location() = location;
 }
diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h
index fefbb3dcb1f..6bc1472b0de 100644
--- a/src/goto-instrument/havoc_utils.h
+++ b/src/goto-instrument/havoc_utils.h
@@ -22,6 +22,7 @@ Date: July 2021
 
 typedef std::set<exprt> modifiest;
 
+/// \brief A class containing utility functions for havocing expressions.
 class havoc_utils_is_constantt : public is_constantt
 {
 public:
@@ -43,19 +44,63 @@ class havoc_utils_is_constantt : public is_constantt
   const modifiest &modifies;
 };
 
-void append_havoc_code(
-  const source_locationt source_location,
-  const modifiest &modifies,
-  goto_programt &dest);
+class havoc_utilst
+{
+public:
+  explicit havoc_utilst(const modifiest &mod) : modifies(mod), is_constant(mod)
+  {
+  }
 
-void append_object_havoc_code_for_expr(
-  const source_locationt source_location,
-  const exprt &expr,
-  goto_programt &dest);
+  /// \brief Append goto instructions to havoc the full `modifies` set
+  ///
+  /// This function invokes `append_havoc_code_for_expr` on each expression in
+  /// the `modifies` set.
+  ///
+  /// \param location The source location to annotate on the havoc instruction
+  /// \param dest The destination goto program to append the instructions to
+  void append_full_havoc_code(
+    const source_locationt location,
+    goto_programt &dest) const;
+
+  /// \brief Append goto instructions to havoc a single expression `expr`
+  ///
+  /// If `expr` is an array index or object dereference expression,
+  /// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`,
+  /// then instructions are generated to havoc the entire underlying object.
+  /// Otherwise, e.g. for a[0] or *(b+i) when `i` is a known constant,
+  /// the instructions are generated to only havoc the scalar value of `expr`.
+  ///
+  /// \param location The source location to annotate on the havoc instruction
+  /// \param expr The expression to havoc
+  /// \param dest The destination goto program to append the instructions to
+  void append_havoc_code_for_expr(
+    const source_locationt location,
+    const exprt &expr,
+    goto_programt &dest) const;
+
+  /// \brief Append goto instructions to havoc the underlying object of `expr`
+  ///
+  /// \param location The source location to annotate on the havoc instruction
+  /// \param expr The expression to havoc
+  /// \param dest The destination goto program to append the instructions to
+  virtual void append_object_havoc_code_for_expr(
+    const source_locationt location,
+    const exprt &expr,
+    goto_programt &dest) const;
+
+  /// \brief Append goto instructions to havoc the value of `expr`
+  ///
+  /// \param location The source location to annotate on the havoc instruction
+  /// \param expr The expression to havoc
+  /// \param dest The destination goto program to append the instructions to
+  virtual void append_scalar_havoc_code_for_expr(
+    const source_locationt location,
+    const exprt &expr,
+    goto_programt &dest) const;
 
-void append_scalar_havoc_code_for_expr(
-  const source_locationt source_location,
-  const exprt &expr,
-  goto_programt &dest);
+protected:
+  const modifiest &modifies;
+  const havoc_utils_is_constantt is_constant;
+};
 
 #endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp
index f0e54ce4e58..922c31a3a0d 100644
--- a/src/goto-instrument/k_induction.cpp
+++ b/src/goto-instrument/k_induction.cpp
@@ -97,7 +97,8 @@ void k_inductiont::process_loop(
 
     // build the havocking code
     goto_programt havoc_code;
-    append_havoc_code(loop_head->source_location, modifies, havoc_code);
+    havoc_utilst havoc_gen(modifies);
+    havoc_gen.append_full_havoc_code(loop_head->source_location, havoc_code);
 
     // unwind to get k+1 copies
     std::vector<goto_programt::targett> iteration_points;
diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp
index 356ea9143f2..c7506aebec8 100644
--- a/src/goto-instrument/loop_utils.cpp
+++ b/src/goto-instrument/loop_utils.cpp
@@ -50,10 +50,11 @@ void get_modifies_lhs(
     const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
     for(const auto &mod : local_may_alias.get(t, ptr.pointer))
     {
+      const typecast_exprt typed_mod{mod, ptr.pointer.type()};
       if(ptr.offset.is_nil())
-        modifies.insert(dereference_exprt{mod});
+        modifies.insert(dereference_exprt{typed_mod});
       else
-        modifies.insert(dereference_exprt{plus_exprt{mod, ptr.offset}});
+        modifies.insert(dereference_exprt{plus_exprt{typed_mod, ptr.offset}});
     }
   }
   else if(lhs.id()==ID_if)