Skip to content

Commit f310308

Browse files
Simplify conditions created in symex_goto
1 parent 46f14a8 commit f310308

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

src/goto-symex/symex_goto.cpp

+12
Original file line numberDiff line numberDiff line change
@@ -487,6 +487,18 @@ static void merge_names(
487487
{
488488
rhs = goto_state_rhs;
489489
}
490+
else if(diff_guard.is_false())
491+
{
492+
if(do_simplify)
493+
simplify(dest_state_rhs, ns);
494+
rhs = dest_state_rhs;
495+
}
496+
else if(diff_guard.is_true())
497+
{
498+
if(do_simplify)
499+
simplify(goto_state_rhs, ns);
500+
rhs = goto_state_rhs;
501+
}
490502
else
491503
{
492504
if(do_simplify)

0 commit comments

Comments
 (0)