Inline get_l1_name

romainbrenguier · romainbrenguier · commit 7128e961e0aa · 2018-12-12T11:23:56.000Z
For ssa_exprt's this always remove_level_2
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -222,7 +222,7 @@ void goto_symex_statet::assignment(
     get_l1_name(l1_rhs);
 
     ssa_exprt l1_lhs(lhs);
-    get_l1_name(l1_lhs);
+    l1_lhs.remove_level_2();
 
     if(run_validation_checks)
     {

Original file line number	Diff line number	Diff line change
`@@ -222,7 +222,7 @@ void goto_symex_statet::assignment(`
`222`	`222`	`get_l1_name(l1_rhs);`
`223`	`223`
`224`	`224`	`ssa_exprt l1_lhs(lhs);`
`225`		`- get_l1_name(l1_lhs);`
	`225`	`+ l1_lhs.remove_level_2();`
`226`	`226`
`227`	`227`	`if(run_validation_checks)`
`228`	`228`	`{`