File tree Expand file tree Collapse file tree 4 files changed +5
-8
lines changed
Expand file tree Collapse file tree 4 files changed +5
-8
lines changed Original file line number Diff line number Diff line change @@ -270,6 +270,6 @@ void invariant_propagationt::simplify(goto_programt &goto_program)
270270 ::simplify (simplified_guard, ns);
271271
272272 if (invariant_set.implies (simplified_guard).is_true ())
273- i_it->set_condition ( true_exprt () );
273+ i_it->condition_nonconst () = true_exprt ();
274274 }
275275}
Original file line number Diff line number Diff line change @@ -112,9 +112,7 @@ void concurrency_instrumentationt::instrument(
112112 }
113113 else if (it->is_assume () || it->is_assert () || it->is_goto ())
114114 {
115- exprt cond = it->get_condition ();
116- instrument (cond);
117- it->set_condition (cond);
115+ instrument (it->condition_nonconst ());
118116 }
119117 else if (it->is_function_call ())
120118 {
Original file line number Diff line number Diff line change @@ -269,7 +269,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
269269 if (it->get_target ()->target_number == it_z->target_number )
270270 {
271271 it->set_target (it_goto_y->get_target ());
272- it->set_condition ( boolean_negate (it->get_condition () ));
272+ it->condition_nonconst () = boolean_negate (it->condition ( ));
273273 it_goto_y->turn_into_skip ();
274274 }
275275 }
Original file line number Diff line number Diff line change @@ -282,9 +282,8 @@ void goto_inlinet::insert_function_body(
282282
283283 if (instruction.has_condition ())
284284 {
285- exprt c = instruction.get_condition ();
286- replace_location (c, target->source_location );
287- instruction.set_condition (c);
285+ replace_location (
286+ instruction.condition_nonconst (), target->source_location );
288287 }
289288 }
290289 }
You can’t perform that action at this time.
0 commit comments