Avoid unecessary simplification

romainbrenguier · romainbrenguier · commit cb0f4eba0958 · 2019-01-11T13:25:06.000Z
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
@@ -489,9 +489,12 @@ static void merge_names(
   }
   else
   {
-    rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
     if(do_simplify)
-      simplify(rhs, ns);
+    {
+      simplify(goto_state_rhs, ns);
+      simplify(dest_state_rhs, ns);
+    }
+    rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
   }
 
   ssa_exprt new_lhs = ssa;

Original file line number	Diff line number	Diff line change
`@@ -489,9 +489,12 @@ static void merge_names(`
`489`	`489`	`}`
`490`	`490`	`else`
`491`	`491`	`{`
`492`		`- rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);`
`493`	`492`	`if(do_simplify)`
`494`		`- simplify(rhs, ns);`
	`493`	`+ {`
	`494`	`+ simplify(goto_state_rhs, ns);`
	`495`	`+ simplify(dest_state_rhs, ns);`
	`496`	`+ }`
	`497`	`+ rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);`
`495`	`498`	`}`
`496`	`499`
`497`	`500`	`ssa_exprt new_lhs = ssa;`