@@ -85,13 +85,12 @@ void symex_slice_by_tracet::slice_by_trace(
85
85
86
86
slice_SSA_steps (equation, implications); // Slice based on implications
87
87
88
- guardt t_guard;
89
88
symex_targett::sourcet empty_source;
90
89
equation.SSA_steps .emplace_front (
91
90
empty_source, goto_trace_stept::typet::ASSUME);
92
91
symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps .front ();
93
92
94
- SSA_step.guard =t_guard. as_expr ();
93
+ SSA_step.guard = true_exprt ();
95
94
SSA_step.ssa_lhs .make_nil ();
96
95
SSA_step.cond_expr .swap (trace_condition);
97
96
@@ -485,7 +484,6 @@ void symex_slice_by_tracet::assign_merges(
485
484
ssa_exprt merge_sym (merge_symbol);
486
485
merge_sym.set_level_2 (merge_count);
487
486
merge_count--;
488
- guardt t_guard;
489
487
symex_targett::sourcet empty_source;
490
488
491
489
exprt merge_copy (*i);
@@ -494,7 +492,7 @@ void symex_slice_by_tracet::assign_merges(
494
492
empty_source, goto_trace_stept::typet::ASSIGNMENT);
495
493
symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps .front ();
496
494
497
- SSA_step.guard =t_guard. as_expr ();
495
+ SSA_step.guard = true_exprt ();
498
496
SSA_step.ssa_lhs =merge_sym;
499
497
SSA_step.ssa_rhs .swap (merge_copy);
500
498
SSA_step.assignment_type =symex_targett::assignment_typet::HIDDEN;
0 commit comments