Skip to content

Commit caff079

Browse files
Infer cond_expr in SSA_assignment_step
This can be deduced fro lhs and rhs without having to give it to the constructor.
1 parent 5a25e47 commit caff079

File tree

3 files changed

+1
-4
lines changed

3 files changed

+1
-4
lines changed

src/goto-symex/ssa_step.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -221,7 +221,6 @@ SSA_assignment_stept::SSA_assignment_stept(
221221
exprt _ssa_full_lhs,
222222
exprt _original_full_lhs,
223223
exprt _ssa_rhs,
224-
exprt _cond_expr,
225224
symex_targett::assignment_typet _assignment_type)
226225
: SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT)
227226
{
@@ -231,7 +230,7 @@ SSA_assignment_stept::SSA_assignment_stept(
231230
original_full_lhs = std::move(_original_full_lhs);
232231
ssa_rhs = std::move(_ssa_rhs);
233232
assignment_type = _assignment_type;
234-
cond_expr = std::move(_cond_expr);
233+
cond_expr = equal_exprt(ssa_lhs, ssa_rhs);
235234
hidden =
236235
assignment_type != symex_targett::assignment_typet::STATE &&
237236
assignment_type !=

src/goto-symex/ssa_step.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,6 @@ class SSA_assignment_stept : public SSA_stept
205205
exprt ssa_full_lhs,
206206
exprt original_full_lhs,
207207
exprt ssa_rhs,
208-
exprt cond_expr,
209208
symex_targett::assignment_typet assignment_type);
210209
};
211210

src/goto-symex/symex_target_equation.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,6 @@ void symex_target_equationt::assignment(
121121
ssa_full_lhs,
122122
original_full_lhs,
123123
ssa_rhs,
124-
equal_exprt(ssa_lhs, ssa_rhs),
125124
assignment_type});
126125

127126
merge_ireps(SSA_steps.back());

0 commit comments

Comments
 (0)