rebase after fixes

Author: Remi Delmas

src/goto-instrument/contracts/contracts.cpp

@@ -308,16 +308,15 @@ void code_contractst::check_apply_loop_contracts(
       goto_function.body, loop_head, snapshot_instructions);
   };
 
-    // Perform write set instrumentation on the entire loop.
-    check_frame_conditions(
-      function_name,
-      goto_function.body,
-      loop_head,
-      loop_end,
-      loop_assigns,
-      // do not skip checks on function parameter assignments
-      false);
-  }
+  // Perform write set instrumentation on the entire loop.
+  check_frame_conditions(
+    function_name,
+    goto_function.body,
+    loop_head,
+    loop_end,
+    loop_assigns,
+    // do not skip checks on function parameter assignments
+    false);
 
   havoc_assigns_targetst havoc_gen(to_havoc, ns);
   havoc_gen.append_full_havoc_code(