Skip to content

Commit 0b6eca3

Browse files
Simplify conditions created in symex_goto
1 parent 6bf0fa5 commit 0b6eca3

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

src/goto-symex/symex_goto.cpp

Lines changed: 12 additions & 0 deletions
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)