Skip to content

Commit 18bf1fc

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 7702d52 commit 18bf1fc

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

src/goto-symex/symex_start_thread.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -68,10 +68,11 @@ 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+
std::piecewise_construct,
73+
std::forward_as_tuple(lhs.get_l1_object_identifier()),
74+
std::forward_as_tuple(lhs, 0));
75+
CHECK_RETURN(emplace_result.second);
7576
state.rename(lhs, ns, goto_symex_statet::L1);
7677
const irep_idt l1_name=lhs.get_l1_object_identifier();
7778
// store it

0 commit comments

Comments
 (0)