diff --git a/regression/contracts-dfcc/invar_assigns_empty/test.desc b/regression/contracts-dfcc/invar_assigns_empty/test.desc
index d727a4b9573..56148a043ab 100644
--- a/regression/contracts-dfcc/invar_assigns_empty/test.desc
+++ b/regression/contracts-dfcc/invar_assigns_empty/test.desc
@@ -6,7 +6,6 @@ main.c
 ^\[main.loop_assigns.\d+\] line 5 Check assigns clause inclusion for loop .*: SUCCESS$
 ^\[main.loop_invariant_base.\d+\] line 5 Check invariant before entry for loop .*: SUCCESS$
 ^\[main.loop_invariant_step.\d+\] line 5 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 5 Check step was unwound for loop .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h
index 56cedd05baa..20cf3f049c3 100644
--- a/src/goto-instrument/contracts/contracts.h
+++ b/src/goto-instrument/contracts/contracts.h
@@ -147,7 +147,7 @@ class code_contractst
     return loop_havoc_set;
   }
 
-  namespacet ns;
+  const namespacet ns;
 
 protected:
   goto_modelt &goto_model;
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 d47e1574d90..d20a80dc759 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
@@ -503,6 +503,10 @@ dfcc_cfg_infot::dfcc_cfg_infot(
 {
   dfcc_loop_nesting_grapht loop_nesting_graph;
   goto_programt &goto_program = goto_function.body;
+
+  // Clean up possible fake loops that are due to do { ... } while(0);
+  simplify_gotos(goto_program, ns);
+
   if(loop_contract_config.apply_loop_contracts)
   {
     messaget log(message_handler);
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
index 79e48791ec2..da3b06dfa86 100644
--- a/src/goto-instrument/contracts/utils.cpp
+++ b/src/goto-instrument/contracts/utils.cpp
@@ -257,7 +257,7 @@ void insert_before_and_update_jumps(
   }
 }
 
-void simplify_gotos(goto_programt &goto_program, namespacet &ns)
+void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
 {
   for(auto &instruction : goto_program.instructions)
   {
@@ -270,7 +270,7 @@ void simplify_gotos(goto_programt &goto_program, namespacet &ns)
 
 bool is_loop_free(
   const goto_programt &goto_program,
-  namespacet &ns,
+  const namespacet &ns,
   messaget &log)
 {
   // create cfg from instruction list
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
index 4fd310627b8..b46f9831cc4 100644
--- a/src/goto-instrument/contracts/utils.h
+++ b/src/goto-instrument/contracts/utils.h
@@ -199,13 +199,13 @@ void insert_before_and_update_jumps(
 
 /// Turns goto instructions `IF cond GOTO label` where the condition
 /// statically simplifies to `false` into SKIP instructions.
-void simplify_gotos(goto_programt &goto_program, namespacet &ns);
+void simplify_gotos(goto_programt &goto_program, const namespacet &ns);
 
 /// Returns true iff the given program is loop-free,
 /// i.e. if each SCC of its CFG contains a single element.
 bool is_loop_free(
   const goto_programt &goto_program,
-  namespacet &ns,
+  const namespacet &ns,
   messaget &log);
 
 /// Returns an \ref irep_idt that essentially says that