diff --git a/regression/contracts-dfcc/loop_contracts_do_while/main.c b/regression/contracts-dfcc/loop_contracts_do_while/main.c
index 8519d3953fb..6cdce8ce510 100644
--- a/regression/contracts-dfcc/loop_contracts_do_while/main.c
+++ b/regression/contracts-dfcc/loop_contracts_do_while/main.c
@@ -5,7 +5,7 @@ int main()
   int x = 0;
 
   do
-    __CPROVER_loop_invariant(0 <= x && x <= 10)
+    __CPROVER_loop_invariant(0 <= x && x < 10)
     {
       x++;
     }
diff --git a/regression/contracts-dfcc/loop_contracts_do_while/nested.desc b/regression/contracts-dfcc/loop_contracts_do_while/nested.desc
index 20cdc6fa135..7a2ee1640c7 100644
--- a/regression/contracts-dfcc/loop_contracts_do_while/nested.desc
+++ b/regression/contracts-dfcc/loop_contracts_do_while/nested.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 nested.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
@@ -6,4 +6,4 @@ nested.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-We spuriously report that x is not assignable.
+We properly skip the instrumentation of both loops.
diff --git a/regression/contracts-dfcc/loop_contracts_do_while/test.desc b/regression/contracts-dfcc/loop_contracts_do_while/test.desc
index dbe8bafe65d..92e2679c437 100644
--- a/regression/contracts-dfcc/loop_contracts_do_while/test.desc
+++ b/regression/contracts-dfcc/loop_contracts_do_while/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc
index 044656dbb72..cda8a3f88b7 100644
--- a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc
+++ b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc
@@ -1,10 +1,11 @@
 CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
 --
-^Found loop with more than one latch instruction$
 --
 This test checks that our loop contract instrumentation first transforms loops
-so as to only have a single loop latch.
+so as to only have a single loop latch, and skips instrumentation if the result
+has no contract.
diff --git a/regression/contracts-dfcc/skip_loop_instrumentation/main.c b/regression/contracts-dfcc/skip_loop_instrumentation/main.c
new file mode 100644
index 00000000000..530f789df68
--- /dev/null
+++ b/regression/contracts-dfcc/skip_loop_instrumentation/main.c
@@ -0,0 +1,29 @@
+int global;
+
+int main()
+{
+  global = 0;
+  int argc = 1;
+  do
+  {
+    int local;
+    global = 1;
+    local = 1;
+    for(int i = 0; i < 1; i++)
+    {
+      local = 1;
+      global = 2;
+      int j = 0;
+      while(j < 1)
+      {
+        local = 1;
+        global = 3;
+        j++;
+      }
+      __CPROVER_assert(global == 3, "case3");
+    }
+    __CPROVER_assert(global == 3, "case3");
+  } while(0);
+  __CPROVER_assert(global == 3, "case1");
+  return 0;
+}
diff --git a/regression/contracts-dfcc/skip_loop_instrumentation/test.desc b/regression/contracts-dfcc/skip_loop_instrumentation/test.desc
new file mode 100644
index 00000000000..95c27f84234
--- /dev/null
+++ b/regression/contracts-dfcc/skip_loop_instrumentation/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test case checks that when the instrumentation of nested loops is skipped, we redirect the write set checks to the
+outer write set.
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
index 97b632cbb70..a42cb1bdc7a 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
@@ -628,6 +628,18 @@ void dfcc_cfg_infot::output(std::ostream &out) const
   }
 }
 
+std::size_t dfcc_cfg_infot::get_first_id_not_skipped_or_top_level_id(
+  const std::size_t loop_id) const
+{
+  if(is_top_level_id(loop_id) || !get_loop_info(loop_id).must_skip())
+  {
+    return loop_id;
+  }
+  return get_first_id_not_skipped_or_top_level_id(
+    get_outer_loop_identifier(loop_id).value_or(top_level_id()));
+}
+
+#include <iostream>
 const exprt &
 dfcc_cfg_infot::get_write_set(goto_programt::const_targett target) const
 {
@@ -635,7 +647,7 @@ dfcc_cfg_infot::get_write_set(goto_programt::const_targett target) const
   PRECONDITION(
     loop_id_opt.has_value() &&
     is_valid_loop_or_top_level_id(loop_id_opt.value()));
-  auto loop_id = loop_id_opt.value();
+  auto loop_id = get_first_id_not_skipped_or_top_level_id(loop_id_opt.value());
   if(is_top_level_id(loop_id))
   {
     return top_level_write_set;
@@ -734,6 +746,11 @@ bool dfcc_cfg_infot::is_top_level_id(const std::size_t id) const
   return id == loop_info_map.size();
 }
 
+size_t dfcc_cfg_infot::top_level_id() const
+{
+  return loop_info_map.size();
+}
+
 bool dfcc_cfg_infot::must_track_decl_or_dead(
   goto_programt::const_targett target) const
 {
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h
index ea4e819a5d2..8de5666a6b7 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h
@@ -144,6 +144,13 @@ class dfcc_loop_infot
   /// this loop. This is the one that must be passed as argument to write set
   /// functions.
   const symbol_exprt addr_of_write_set_var;
+
+  /// Returns true if the loop has no invariant and no decreases clause
+  /// and its instrumentation must be skipped.
+  const bool must_skip() const
+  {
+    return invariant.is_nil() && decreases.empty();
+  }
 };
 
 /// Computes natural loops, enforces normal form conditions, computes the
@@ -248,7 +255,9 @@ class dfcc_cfg_infot
   /// \brief Returns the loop info for that loop_id.
   const dfcc_loop_infot &get_loop_info(const std::size_t loop_id) const;
 
-  /// \brief Returns the write set variable for that instruction.
+  /// \brief Returns the write set variable to use for the given instruction
+  /// Returns the write set for the loop, or one of the outer loops,
+  /// or top level, passing through all loops that are [must_skip]
   const exprt &get_write_set(goto_programt::const_targett target) const;
 
   /// \brief Returns the set of local variable for the scope where that
@@ -270,6 +279,11 @@ class dfcc_cfg_infot
     return topsorted_loops;
   }
 
+  /// \brief Returns the id of the first outer loop (including this one) that
+  /// is not skipped, or the top level id.
+  std::size_t
+  get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const;
+
   /// Finds the DFCC id of the loop that contains the given loop, returns
   /// nullopt when the loop has no outer loop.
   const std::optional<std::size_t>
@@ -314,6 +328,9 @@ class dfcc_cfg_infot
   /// True iff \p id is in the valid range for a loop id for this function.
   bool is_top_level_id(const std::size_t id) const;
 
+  /// Returns the top level ID
+  size_t top_level_id() const;
+
   /// Loop identifiers sorted from most deeply nested to less deeply nested
   std::vector<std::size_t> topsorted_loops;
 
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
index 707feaedffd..b37d6a7c55c 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
@@ -1239,7 +1239,7 @@ void dfcc_instrumentt::apply_loop_contracts(
   for(const auto &loop_id : cfg_info.get_loops_toposorted())
   {
     const auto &loop = cfg_info.get_loop_info(loop_id);
-    if(loop.invariant.is_nil() && loop.decreases.empty())
+    if(loop.must_skip())
     {
       // skip loops that do not have contracts
       log.warning() << "loop " << function_id << "." << loop.cbmc_loop_id