Skip to content

Commit 41f7001

Browse files
Simplify lhs in build goto trace
Avoid lhs of the form `{array[0], array[1]}[0]`
1 parent b17a422 commit 41f7001

File tree

1 file changed

+7
-5
lines changed

1 file changed

+7
-5
lines changed

src/goto-symex/build_goto_trace.cpp

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -370,11 +370,13 @@ void build_goto_trace(
370370

371371
if(SSA_step.original_full_lhs.is_not_nil())
372372
{
373-
goto_trace_step.full_lhs = build_full_lhs_rec(
374-
decision_procedure,
375-
ns,
376-
SSA_step.original_full_lhs,
377-
SSA_step.ssa_full_lhs);
373+
goto_trace_step.full_lhs = simplify_expr(
374+
build_full_lhs_rec(
375+
decision_procedure,
376+
ns,
377+
SSA_step.original_full_lhs,
378+
SSA_step.ssa_full_lhs),
379+
ns);
378380
replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
379381
}
380382

0 commit comments

Comments
 (0)