diff --git a/regression/contracts/invar_check_break_fail/test.desc b/regression/contracts/invar_check_break_fail/test.desc
index 8dcb8ede040..705739ed7aa 100644
--- a/regression/contracts/invar_check_break_fail/test.desc
+++ b/regression/contracts/invar_check_break_fail/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_break_pass/test.desc b/regression/contracts/invar_check_break_pass/test.desc
index ea11f37bf07..272f26256f3 100644
--- a/regression/contracts/invar_check_break_pass/test.desc
+++ b/regression/contracts/invar_check_break_pass/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_continue/test.desc b/regression/contracts/invar_check_continue/test.desc
index 654d25185aa..f29ca70fd67 100644
--- a/regression/contracts/invar_check_continue/test.desc
+++ b/regression/contracts/invar_check_continue/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_large/test.desc b/regression/contracts/invar_check_large/test.desc
index f5c18f62587..3b84ac40658 100644
--- a/regression/contracts/invar_check_large/test.desc
+++ b/regression/contracts/invar_check_large/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc
index 0b2578bc594..f5522104e07 100644
--- a/regression/contracts/invar_check_multiple_loops/test.desc
+++ b/regression/contracts/invar_check_multiple_loops/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc
index e1f59d8e91d..2035a258ee6 100644
--- a/regression/contracts/invar_check_nested_loops/test.desc
+++ b/regression/contracts/invar_check_nested_loops/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_pointer_modifies-01/test.desc b/regression/contracts/invar_check_pointer_modifies-01/test.desc
index 818db63cf95..f9be5027db7 100644
--- a/regression/contracts/invar_check_pointer_modifies-01/test.desc
+++ b/regression/contracts/invar_check_pointer_modifies-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts --pointer-check
+--apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_pointer_modifies-02/test.desc b/regression/contracts/invar_check_pointer_modifies-02/test.desc
index 8cf754528bc..d96eca605ae 100644
--- a/regression/contracts/invar_check_pointer_modifies-02/test.desc
+++ b/regression/contracts/invar_check_pointer_modifies-02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts --pointer-check
+--apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_sufficiency/test.desc b/regression/contracts/invar_check_sufficiency/test.desc
index a76c7b312b4..3c7c3b3bc33 100644
--- a/regression/contracts/invar_check_sufficiency/test.desc
+++ b/regression/contracts/invar_check_sufficiency/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_dynamic_struct_member/test.desc b/regression/contracts/invar_dynamic_struct_member/test.desc
index 386750ad98f..f312b930d1b 100644
--- a/regression/contracts/invar_dynamic_struct_member/test.desc
+++ b/regression/contracts/invar_dynamic_struct_member/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_array/test.desc b/regression/contracts/invar_havoc_dynamic_array/test.desc
index 744b830523d..b86d0b35c5c 100644
--- a/regression/contracts/invar_havoc_dynamic_array/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
index ac9229ceb52..3c3fcb5f8e9 100644
--- a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc
index 37add427a1a..174fa755423 100644
--- a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
index 5378d8a9fbd..f57ca4872a7 100644
--- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc
index 18f3bf70144..0e180ad0d42 100644
--- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_array/test.desc b/regression/contracts/invar_havoc_static_array/test.desc
index 7a660288649..3c37f31945c 100644
--- a/regression/contracts/invar_havoc_static_array/test.desc
+++ b/regression/contracts/invar_havoc_static_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_array_const_idx/test.desc b/regression/contracts/invar_havoc_static_array_const_idx/test.desc
index b8aeb51972e..7004c2b0d0d 100644
--- a/regression/contracts/invar_havoc_static_array_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_static_array_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array/test.desc
index 5c5ae80144e..b1b8b58c5e5 100644
--- a/regression/contracts/invar_havoc_static_multi-dim_array/test.desc
+++ b/regression/contracts/invar_havoc_static_multi-dim_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc
index da6227c565e..7a315d41510 100644
--- a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc
index fffb2a43c19..1c0ebbdea38 100644
--- a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_loop_constant_fail/test.desc b/regression/contracts/invar_loop_constant_fail/test.desc
index 1411c8a199b..3f1753aba33 100644
--- a/regression/contracts/invar_loop_constant_fail/test.desc
+++ b/regression/contracts/invar_loop_constant_fail/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_loop_constant_no_modify/test.desc b/regression/contracts/invar_loop_constant_no_modify/test.desc
index fa38c4d19e5..d169ad4403b 100644
--- a/regression/contracts/invar_loop_constant_no_modify/test.desc
+++ b/regression/contracts/invar_loop_constant_no_modify/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_loop_constant_pass/test.desc b/regression/contracts/invar_loop_constant_pass/test.desc
index b272e4d3ecd..e0538966c1d 100644
--- a/regression/contracts/invar_loop_constant_pass/test.desc
+++ b/regression/contracts/invar_loop_constant_pass/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_struct_member/test.desc b/regression/contracts/invar_struct_member/test.desc
index ce0503ebba7..c969cfcc6cb 100644
--- a/regression/contracts/invar_struct_member/test.desc
+++ b/regression/contracts/invar_struct_member/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invariant_side_effects/test.desc b/regression/contracts/invariant_side_effects/test.desc
index e15f86c30e0..3e6caba882f 100644
--- a/regression/contracts/invariant_side_effects/test.desc
+++ b/regression/contracts/invariant_side_effects/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/quantifiers-loop-01/test.desc b/regression/contracts/quantifiers-loop-01/test.desc
index be46c230b33..ebe5becbfa6 100644
--- a/regression/contracts/quantifiers-loop-01/test.desc
+++ b/regression/contracts/quantifiers-loop-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] line .* Check loop invariant before entry: SUCCESS
diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc
index 1e28824258d..237838679dc 100644
--- a/regression/contracts/quantifiers-loop-02/test.desc
+++ b/regression/contracts/quantifiers-loop-02/test.desc
@@ -1,6 +1,6 @@
-CORE
+CORE smt-backend
 main.c
---enforce-all-contracts _ --z3
+--apply-loop-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS
diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc
index 429c07e0ec2..9c3f9f7b76c 100644
--- a/regression/contracts/quantifiers-loop-03/test.desc
+++ b/regression/contracts/quantifiers-loop-03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] line .* Check loop invariant before entry: SUCCESS
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index 1dafb783fdf..e6d5bb35a3c 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -1186,6 +1186,12 @@ bool code_contractst::replace_calls(
   return false;
 }
 
+void code_contractst::apply_loop_contracts()
+{
+  for(auto &goto_function : goto_functions.function_map)
+    apply_loop_contract(goto_function.first, goto_function.second);
+}
+
 bool code_contractst::replace_calls()
 {
   std::set<std::string> funs_to_replace;
@@ -1204,8 +1210,6 @@ bool code_contractst::enforce_contracts()
   {
     if(has_contract(goto_function.first))
       funs_to_enforce.insert(id2string(goto_function.first));
-    else
-      apply_loop_contract(goto_function.first, goto_function.second);
   }
   return enforce_contracts(funs_to_enforce);
 }
@@ -1225,7 +1229,6 @@ bool code_contractst::enforce_contracts(
                   << messaget::eom;
       continue;
     }
-    apply_loop_contract(goto_function->first, goto_function->second);
 
     if(!has_contract(fun))
     {
diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h
index f9da1d19360..a70acad5b75 100644
--- a/src/goto-instrument/code_contracts.h
+++ b/src/goto-instrument/code_contracts.h
@@ -90,6 +90,8 @@ class code_contractst
   /// \return `true` on failure, `false` otherwise
   bool replace_calls();
 
+  void apply_loop_contracts();
+
   const symbolt &new_tmp_symbol(
     const typet &type,
     const source_locationt &source_location,
@@ -216,6 +218,11 @@ class code_contractst
     const irep_idt &mode);
 };
 
+#define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
+#define HELP_LOOP_CONTRACTS                                                    \
+  " --apply-loop-contracts\n"                                                  \
+  "                              check and use loop contracts when provided\n"
+
 #define FLAG_REPLACE_CALL "replace-call-with-contract"
 #define HELP_REPLACE_CALL                                                      \
   " --replace-call-with-contract <fun>\n"                                      \
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 243ff623951..ad6881ed206 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1149,7 +1149,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   }
 
   if(
-    cmdline.isset(FLAG_REPLACE_CALL) || cmdline.isset(FLAG_REPLACE_ALL_CALLS) ||
+    cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
+    cmdline.isset(FLAG_REPLACE_ALL_CALLS) ||
     cmdline.isset(FLAG_ENFORCE_CONTRACT) ||
     cmdline.isset(FLAG_ENFORCE_ALL_CONTRACTS))
   {
@@ -1180,6 +1181,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     if(cmdline.isset(FLAG_ENFORCE_ALL_CONTRACTS))
       if(cont.enforce_contracts())
         exit(CPROVER_EXIT_USAGE_ERROR);
+
+    if(cmdline.isset(FLAG_LOOP_CONTRACTS))
+      cont.apply_loop_contracts();
   }
 
   if(cmdline.isset("value-set-fi-fp-removal"))
@@ -1868,7 +1872,8 @@ void goto_instrument_parse_optionst::help()
     " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
     HELP_REPLACE_CALLS
     "\n"
-    "Function contracts and invariants:\n"
+    "Code contracts:\n"
+    HELP_LOOP_CONTRACTS
     HELP_REPLACE_CALL
     HELP_REPLACE_ALL_CALLS
     HELP_ENFORCE_CONTRACT
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index fec804fa0f3..0002b11e5ce 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -99,6 +99,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
   "(horn)(skip-loops):(model-argc-argv):" \
+  "(" FLAG_LOOP_CONTRACTS ")" \
   "(" FLAG_REPLACE_CALL "):" \
   "(" FLAG_REPLACE_ALL_CALLS ")" \
   "(" FLAG_ENFORCE_CONTRACT "):" \