fix recording old variant value at the beginning of loop body

SaswatPadhi · SaswatPadhi · commit 1b34d7ca8587 · 2021-11-09T00:24:21.000Z
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -209,7 +209,10 @@ void code_contractst::check_apply_loop_contracts(
       converter.goto_convert(old_decreases_assignment, havoc_code, mode);
     }
 
-    goto_function.body.destructive_insert(std::next(loop_head), havoc_code);
+    const auto head_loc = loop_head->source_location();
+    while(loop_head->source_location() == head_loc)
+      loop_head = std::next(loop_head);
+    goto_function.body.destructive_insert(loop_head, havoc_code);
   }
 
   // Generate: assert(invariant) just after the loop exits

Original file line number	Diff line number	Diff line change
`@@ -209,7 +209,10 @@ void code_contractst::check_apply_loop_contracts(`
`209`	`209`	`converter.goto_convert(old_decreases_assignment, havoc_code, mode);`
`210`	`210`	`}`
`211`	`211`
`212`		`- goto_function.body.destructive_insert(std::next(loop_head), havoc_code);`
	`212`	`+ const auto head_loc = loop_head->source_location();`
	`213`	`+ while(loop_head->source_location() == head_loc)`
	`214`	`+ loop_head = std::next(loop_head);`
	`215`	`+ goto_function.body.destructive_insert(loop_head, havoc_code);`
`213`	`216`	`}`
`214`	`217`
`215`	`218`	`// Generate: assert(invariant) just after the loop exits`