diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp
index bfc012effdc..b11cdad6f22 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp
@@ -100,6 +100,7 @@ const symbolt &dfcc_utilst::create_symbol(
     source_location,
     mode,
     goto_model.symbol_table);
+  symbol.module = module;
   symbol.is_lvalue = true;
   symbol.is_state_var = true;
   symbol.is_thread_local = true;
@@ -125,6 +126,7 @@ const symbolt &dfcc_utilst::create_static_symbol(
     source_location,
     mode,
     goto_model.symbol_table);
+  symbol.module = module;
   symbol.is_static_lifetime = true;
   symbol.value = initial_value;
   symbol.value.set(ID_C_no_nondet_initialization, no_nondet_initialization);
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
index d0b5df0913d..6ef75380955 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
@@ -228,8 +228,8 @@ dfcc_wrapper_programt::dfcc_wrapper_programt(
                            id2string(wrapper_symbol.name),
                            "__contract_return_value",
                            wrapper_symbol.location,
-                           wrapper_symbol.module,
                            wrapper_symbol.mode,
+                           wrapper_symbol.module,
                            false)
                          .symbol_expr();