diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc
index 425e9705f27..616e2b670ab 100644
--- a/regression/contracts/assigns_enforce_free_dead/test.desc
+++ b/regression/contracts/assigns_enforce_free_dead/test.desc
@@ -29,7 +29,9 @@ main.c
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$
-^.*tmp_cc\$\d+.*: FAILURE$
+^.*__car_valid.*: FAILURE$
+^.*__car_lb.*: FAILURE$
+^.*__car_ub.*: FAILURE$
 --
 Checks that invalidated CARs are correctly tracked on `free` and `DEAD`.
 
@@ -40,4 +42,4 @@ We also check (using positive regex matches above) that
 `**p` should be assignable in one case and should not be assignable in the other.
 
 Finally, we check that there should be no "internal" assertion failures
-on `tmp_cc` variables used to track CARs.
+on `__car_valid`, `__car_ub`, `__car_lb` variables used to track CARs.
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c
index db97d407e56..cceba46be58 100644
--- a/regression/contracts/quantifiers-forall-ensures-enforce/main.c
+++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c
@@ -23,7 +23,7 @@ int f1(int *arr, int len)
 int main()
 {
   int len;
-  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+  __CPROVER_assume(0 < len && len <= MAX_LEN);
 
   int *arr = malloc(len * sizeof(int));
   f1(arr, len);
diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index c4e0ba536f9..d02daea3560 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/src/goto-instrument/contracts/assigns.cpp
@@ -12,6 +12,7 @@ Date: July 2021
 /// Specify write set in code contracts
 
 #include "assigns.h"
+#include "utils.h"
 
 #include <analyses/call_graph.h>
 
@@ -52,6 +53,7 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
 }
 
 const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol(
+  const std::string &prefix,
   const typet &type,
   const source_locationt &location) const
 {
@@ -59,7 +61,8 @@ const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol(
     type,
     location,
     parent.symbol_table.lookup_ref(parent.function_name).mode,
-    parent.symbol_table);
+    parent.symbol_table,
+    prefix);
 }
 
 assigns_clauset::conditional_address_ranget::conditional_address_ranget(
@@ -70,11 +73,13 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget(
     parent(parent),
     slice(normalize_to_slice(expr, parent.ns)),
     validity_condition_var(
-      generate_new_symbol(bool_typet(), location).symbol_expr()),
+      generate_new_symbol("__car_valid", bool_typet(), location).symbol_expr()),
     lower_bound_address_var(
-      generate_new_symbol(slice.first.type(), location).symbol_expr()),
+      generate_new_symbol("__car_lb", slice.first.type(), location)
+        .symbol_expr()),
     upper_bound_address_var(
-      generate_new_symbol(slice.first.type(), location).symbol_expr())
+      generate_new_symbol("__car_ub", slice.first.type(), location)
+        .symbol_expr())
 {
 }
 
@@ -83,41 +88,54 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   const
 {
   goto_programt instructions;
-
-  instructions.add(goto_programt::make_decl(validity_condition_var, location));
-  instructions.add(goto_programt::make_decl(lower_bound_address_var, location));
-  instructions.add(goto_programt::make_decl(upper_bound_address_var, location));
+  // adding pragmas to the location to selectively disable checks
+  // where it is sound to do so
+  source_locationt location_no_checks = location;
+  disable_pointer_checks(location_no_checks);
+
+  instructions.add(
+    goto_programt::make_decl(validity_condition_var, location_no_checks));
+  instructions.add(
+    goto_programt::make_decl(lower_bound_address_var, location_no_checks));
+  instructions.add(
+    goto_programt::make_decl(upper_bound_address_var, location_no_checks));
 
   instructions.add(goto_programt::make_assignment(
     lower_bound_address_var,
     null_pointer_exprt{to_pointer_type(slice.first.type())},
-    location));
+    location_no_checks));
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
     null_pointer_exprt{to_pointer_type(slice.first.type())},
-    location));
+    location_no_checks));
 
   goto_programt skip_program;
-  const auto skip_target = skip_program.add(goto_programt::make_skip(location));
+  const auto skip_target =
+    skip_program.add(goto_programt::make_skip(location_no_checks));
 
   const auto validity_check_expr =
     and_exprt{all_dereferences_are_valid(source_expr, parent.ns),
               w_ok_exprt{slice.first, slice.second}};
   instructions.add(goto_programt::make_assignment(
-    validity_condition_var, validity_check_expr, location));
+    validity_condition_var, validity_check_expr, location_no_checks));
 
   instructions.add(goto_programt::make_goto(
-    skip_target, not_exprt{validity_condition_var}, location));
+    skip_target, not_exprt{validity_condition_var}, location_no_checks));
 
   instructions.add(goto_programt::make_assignment(
-    lower_bound_address_var, slice.first, location));
+    lower_bound_address_var, slice.first, location_no_checks));
+
+  // the computation of the CAR upper bound can overflow into the object ID bits
+  // of the pointer with very large allocation sizes.
+  // We enable pointer overflow checks to detect such cases.
+  source_locationt location_overflow_check = location;
+  location_overflow_check.add_pragma("enable:pointer-overflow-check");
 
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
     minus_exprt{plus_exprt{slice.first, slice.second},
                 from_integer(1, slice.second.type())},
-    location));
-
+    location_overflow_check));
   instructions.destructive_append(skip_program);
 
   // The assignments above are only performed on locally defined temporaries
@@ -130,14 +148,16 @@ const exprt
 assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check(
   const conditional_address_ranget &lhs) const
 {
+  // remark: both lb and ub are derived from the same object so checking
+  // same_object(upper_bound_address_var, lhs.upper_bound_address_var)
+  // is redundant
   return conjunction(
     {validity_condition_var,
      same_object(lower_bound_address_var, lhs.lower_bound_address_var),
-     same_object(lhs.upper_bound_address_var, upper_bound_address_var),
-     less_than_or_equal_exprt{lower_bound_address_var,
-                              lhs.lower_bound_address_var},
-     less_than_or_equal_exprt{lhs.upper_bound_address_var,
-                              upper_bound_address_var}});
+     less_than_or_equal_exprt{pointer_offset(lower_bound_address_var),
+                              pointer_offset(lhs.lower_bound_address_var)},
+     less_than_or_equal_exprt{pointer_offset(lhs.upper_bound_address_var),
+                              pointer_offset(upper_bound_address_var)}});
 }
 
 assigns_clauset::assigns_clauset(
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index f076a632feb..883eee8c8e2 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -60,8 +60,10 @@ class assigns_clauset
     const exprt
     generate_unsafe_inclusion_check(const conditional_address_ranget &) const;
 
-    const symbolt
-    generate_new_symbol(const typet &, const source_locationt &) const;
+    const symbolt generate_new_symbol(
+      const std::string &prefix,
+      const typet &,
+      const source_locationt &) const;
 
     friend class assigns_clauset;
   };
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 26df2dfbfb3..0d5424c9df6 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -911,6 +911,8 @@ void code_contractst::instrument_call_statement(
   }
   else if(callee_name == "free")
   {
+    source_locationt location_no_checks = instruction_it->source_location();
+    disable_pointer_checks(location_no_checks);
     const auto free_car = add_inclusion_check(
       body,
       assigns,
@@ -920,10 +922,9 @@ void code_contractst::instrument_call_statement(
     // skip all invalidation business if we're freeing invalid memory
     goto_programt alias_checking_instructions, skip_program;
     alias_checking_instructions.add(goto_programt::make_goto(
-      skip_program.add(
-        goto_programt::make_skip(instruction_it->source_location())),
+      skip_program.add(goto_programt::make_skip(location_no_checks)),
       not_exprt{free_car.validity_condition_var},
-      instruction_it->source_location()));
+      location_no_checks));
 
     // Since the argument to free may be an "alias" (but not identical)
     // to existing CARs' source_expr, structural equality wouldn't work.
@@ -936,14 +937,15 @@ void code_contractst::instrument_call_statement(
       const auto object_validity_var_addr =
         new_tmp_symbol(
           pointer_type(bool_typet{}),
-          instruction_it->source_location(),
+          location_no_checks,
           symbol_table.lookup_ref(function).mode,
-          symbol_table)
+          symbol_table,
+          "__car_valid")
           .symbol_expr();
       write_set_validity_addrs.insert(object_validity_var_addr);
 
-      alias_checking_instructions.add(goto_programt::make_decl(
-        object_validity_var_addr, instruction_it->source_location()));
+      alias_checking_instructions.add(
+        goto_programt::make_decl(object_validity_var_addr, location_no_checks));
       // if the CAR was defined on the same_object as the one being `free`d,
       // record its validity variable's address, otherwise record NULL
       alias_checking_instructions.add(goto_programt::make_assignment(
@@ -955,7 +957,7 @@ void code_contractst::instrument_call_statement(
               free_car.lower_bound_address_var, w_car.lower_bound_address_var)},
           address_of_exprt{w_car.validity_condition_var},
           null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}},
-        instruction_it->source_location()));
+        location_no_checks));
     }
 
     alias_checking_instructions.destructive_append(skip_program);
@@ -971,24 +973,22 @@ void code_contractst::instrument_call_statement(
     goto_programt invalidation_instructions;
     skip_program.clear();
     invalidation_instructions.add(goto_programt::make_goto(
-      skip_program.add(
-        goto_programt::make_skip(instruction_it->source_location())),
+      skip_program.add(goto_programt::make_skip(location_no_checks)),
       not_exprt{free_car.validity_condition_var},
-      instruction_it->source_location()));
+      location_no_checks));
 
     // invalidate all recorded CAR validity variables
     for(const auto &w_car_validity_addr : write_set_validity_addrs)
     {
       goto_programt w_car_skip_program;
       invalidation_instructions.add(goto_programt::make_goto(
-        w_car_skip_program.add(
-          goto_programt::make_skip(instruction_it->source_location())),
+        w_car_skip_program.add(goto_programt::make_skip(location_no_checks)),
         null_pointer(w_car_validity_addr),
-        instruction_it->source_location()));
+        location_no_checks));
       invalidation_instructions.add(goto_programt::make_assignment(
         dereference_exprt{w_car_validity_addr},
         false_exprt{},
-        instruction_it->source_location()));
+        location_no_checks));
       invalidation_instructions.destructive_append(w_car_skip_program);
     }
 
@@ -1174,6 +1174,9 @@ void code_contractst::check_frame_conditions(
     else if(instruction_it->is_dead())
     {
       const auto &symbol = instruction_it->dead_symbol();
+      source_locationt location_no_checks = instruction_it->source_location();
+      disable_pointer_checks(location_no_checks);
+
       // CAR equality and hash are defined on source_expr alone,
       // therefore this temporary CAR should be "found"
       const auto &symbol_car = assigns.get_write_set().find(
@@ -1227,10 +1230,13 @@ code_contractst::add_inclusion_check(
     program, instruction_it, snapshot_instructions);
 
   goto_programt assertion;
-  assertion.add(goto_programt::make_assertion(
-    assigns.generate_inclusion_check(car), instruction_it->source_location()));
-  assertion.instructions.back().source_location_nonconst().set_comment(
+  source_locationt location_no_checks =
+    instruction_it->source_location_nonconst();
+  disable_pointer_checks(location_no_checks);
+  location_no_checks.set_comment(
     "Check that " + from_expr(ns, expr.id(), expr) + " is assignable");
+  assertion.add(goto_programt::make_assertion(
+    assigns.generate_inclusion_check(car), location_no_checks));
   insert_before_swap_and_advance(program, instruction_it, assertion);
 
   return car;
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
index c39cf81da43..95185dd4dd1 100644
--- a/src/goto-instrument/contracts/utils.cpp
+++ b/src/goto-instrument/contracts/utils.cpp
@@ -142,13 +142,24 @@ const symbolt &new_tmp_symbol(
   const typet &type,
   const source_locationt &location,
   const irep_idt &mode,
-  symbol_table_baset &symtab)
+  symbol_table_baset &symtab,
+  std::string suffix,
+  bool is_auxiliary)
 {
-  return get_fresh_aux_symbol(
+  symbolt &new_symbol = get_fresh_aux_symbol(
     type,
-    id2string(location.get_function()) + "::tmp_cc",
-    "tmp_cc",
+    id2string(location.get_function()) + "::",
+    suffix,
     location,
     mode,
     symtab);
+  new_symbol.is_auxiliary = is_auxiliary;
+  return new_symbol;
+}
+
+void disable_pointer_checks(source_locationt &source_location)
+{
+  source_location.add_pragma("disable:pointer-check");
+  source_location.add_pragma("disable:pointer-primitive-check");
+  source_location.add_pragma("disable:pointer-overflow-check");
 }
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
index 70b691aec66..589ab0981b2 100644
--- a/src/goto-instrument/contracts/utils.h
+++ b/src/goto-instrument/contracts/utils.h
@@ -105,17 +105,24 @@ void insert_before_swap_and_advance(
   goto_programt::targett &target,
   goto_programt &payload);
 
-/// \brief Adds a new temporary symbol to the symbol table.
+/// \brief Adds a fresh and uniquely named symbol to the symbol table.
 ///
 /// \param type: The type of the new symbol.
 /// \param location: The source location for the new symbol.
 /// \param mode: The mode for the new symbol, e.g. ID_C, ID_java.
 /// \param symtab: The symbol table to which the new symbol is to be added.
+/// \param suffix: Suffix to use to generate the unique name
+/// \param is_auxiliary: Do not print symbol in traces if true (default = false)
 /// \return The new symbolt object.
 const symbolt &new_tmp_symbol(
   const typet &type,
   const source_locationt &location,
   const irep_idt &mode,
-  symbol_table_baset &symtab);
+  symbol_table_baset &symtab,
+  std::string suffix = "tmp_cc",
+  bool is_auxiliary = false);
+
+/// Add disable pragmas for all pointer checks on the given location
+void disable_pointer_checks(source_locationt &source_location);
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H