Symex: Simplify left-hand side

tautschnig · tautschnig · commit 23853fe7342e · 2023-05-04T11:20:52.000Z
With #7622 we may have syntactically changed the type on the right-hand side via simplification. To maintain syntactic type equality we need to apply simplifications on the left-hand side as well. See https://github.com/awslabs/aws-c-common/actions/runs/4822448417 for an example where this failed after #7622.
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -84,6 +84,8 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
 
   // the type might need renaming
   rename<L2>(lhs.type(), l1_identifier, ns);
+  if(rhs_is_simplified)
+    simplify(lhs, ns);
   lhs.update_type();
   if(run_validation_checks)
   {

Original file line number	Diff line number	Diff line change
`@@ -84,6 +84,8 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(`
`84`	`84`
`85`	`85`	`// the type might need renaming`
`86`	`86`	`rename<L2>(lhs.type(), l1_identifier, ns);`
	`87`	`+ if(rhs_is_simplified)`
	`88`	`+ simplify(lhs, ns);`
`87`	`89`	`lhs.update_type();`
`88`	`90`	`if(run_validation_checks)`
`89`	`91`	`{`