Skip to content

Commit fffba8b

Browse files
committed
Fix guards of havoc assignments
This was previously taking only the innermost if condition into account for nested ternary expressions, due to disarding the outer conditions.
1 parent cdea666 commit fffba8b

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/goto-symex/symex_other.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,11 +46,11 @@ void goto_symext::havoc_rec(
4646
{
4747
const if_exprt &if_expr=to_if_expr(dest);
4848

49-
guardt guard_t=state.guard;
49+
guardt guard_t = guard;
5050
guard_t.add(if_expr.cond());
5151
havoc_rec(state, guard_t, if_expr.true_case());
5252

53-
guardt guard_f=state.guard;
53+
guardt guard_f = guard;
5454
guard_f.add(not_exprt(if_expr.cond()));
5555
havoc_rec(state, guard_f, if_expr.false_case());
5656
}

0 commit comments

Comments
 (0)