CONTRACTS: add inductive checks for assigns clauses

Author: qinheping

src/goto-instrument/contracts/contracts.cpp

@@ -257,8 +257,11 @@ void code_contractst::check_apply_loop_contracts(
 
   // Insert instrumentation
   // This must be done before havocing the write set.
+<<<<<<< HEAD
   // FIXME: this is not true for write set targets that
   // might depend on other write set targets.
+=======
+>>>>>>> aa06faf8b4 (CONTRACTS: add inductive checks for assigns clauses)
   goto_function.body.destructive_insert(
     std::next(loop_head), snapshot_instructions);