Skip to content

Commit 8abb3c8

Browse files
Replace insert by emplace and UNREACHABLE by CHECK_RETURN
Using emplace avoids a call to make_pair, and CHECK_RETURN is more adapted to the situation were we check the return value of insert/emplace.
1 parent 107e1ae commit 8abb3c8

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

src/goto-symex/symex_start_thread.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -68,10 +68,9 @@ void goto_symext::symex_start_thread(statet &state)
6868
lhs.set_level_0(t);
6969

7070
// set up L1 name
71-
if(!state.level1.current_names.insert(
72-
std::make_pair(lhs.get_l1_object_identifier(),
73-
std::make_pair(lhs, 0))).second)
74-
UNREACHABLE;
71+
auto emplace_result = state.level1.current_names.emplace(
72+
lhs.get_l1_object_identifier(), std::make_pair(lhs, 0));
73+
CHECK_RETURN(emplace_result.second);
7574
state.rename(lhs, ns, goto_symex_statet::L1);
7675
const irep_idt l1_name=lhs.get_l1_object_identifier();
7776
// store it

0 commit comments

Comments
 (0)