fix loop assign

thanhnguyen-aws · thanhnguyen-aws · commit 38176263b7cc · 2025-06-18T08:17:32.000-07:00
diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp
@@ -1078,7 +1078,7 @@ void goto_convertt::convert_loop_contracts(
   if(assigns.is_not_nil())
   {
     PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
-    loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
+    loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns);
   }
 
   auto invariant =

Original file line number	Diff line number	Diff line change
`@@ -1078,7 +1078,7 @@ void goto_convertt::convert_loop_contracts(`
`1078`	`1078`	`if(assigns.is_not_nil())`
`1079`	`1079`	`{`
`1080`	`1080`	`PRECONDITION(loop->is_goto() \|\| loop->is_incomplete_goto());`
`1081`		`- loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());`
	`1081`	`+ loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns);`
`1082`	`1082`	`}`
`1083`	`1083`
`1084`	`1084`	`auto invariant =`