fix for ignored assignments

kroening · kroening · commit 92004d6bda9f · 2022-03-09T11:38:12.000Z
diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp
@@ -282,9 +282,13 @@ void state_encodingt::operator()(
       auto rhs = loc->assign_rhs();
       if(lhs.type().id() == ID_array)
       {
+        // skip
+        dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
       }
       else if(lhs.type().id() == ID_struct_tag)
       {
+        // skip
+        dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
       }
       else
         dest << assignment_constraint(loc, std::move(lhs), std::move(rhs));

Original file line number	Diff line number	Diff line change
`@@ -282,9 +282,13 @@ void state_encodingt::operator()(`
`282`	`282`	`auto rhs = loc->assign_rhs();`
`283`	`283`	`if(lhs.type().id() == ID_array)`
`284`	`284`	`{`
	`285`	`+ // skip`
	`286`	`+ dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));`
`285`	`287`	`}`
`286`	`288`	`else if(lhs.type().id() == ID_struct_tag)`
`287`	`289`	`{`
	`290`	`+ // skip`
	`291`	`+ dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));`
`288`	`292`	`}`
`289`	`293`	`else`
`290`	`294`	`dest << assignment_constraint(loc, std::move(lhs), std::move(rhs));`