File tree Expand file tree Collapse file tree 1 file changed +11
-4
lines changed Expand file tree Collapse file tree 1 file changed +11
-4
lines changed Original file line number Diff line number Diff line change @@ -91,8 +91,8 @@ class range_domaint:public range_domain_baset
9191 const_iterator end () const { return data.end (); }
9292 const_iterator cend () const { return data.end (); }
9393
94- template < typename T>
95- void push_back (T &&v) { data.push_back (std::forward<T> (v)); }
94+ void push_back ( const sub_typet::value_type &v) { data. push_back (v); }
95+ void push_back (sub_typet::value_type &&v) { data.push_back (std::move (v)); }
9696};
9797
9898class array_exprt ;
@@ -304,8 +304,15 @@ class guarded_range_domaint:public range_domain_baset
304304 const_iterator end () const { return data.end (); }
305305 const_iterator cend () const { return data.end (); }
306306
307- template <typename T>
308- iterator insert (T &&v) { return data.insert (std::forward<T>(v)); }
307+ iterator insert (const sub_typet::value_type &v)
308+ {
309+ return data.insert (v);
310+ }
311+
312+ iterator insert (sub_typet::value_type &&v)
313+ {
314+ return data.insert (std::move (v));
315+ }
309316};
310317
311318class rw_guarded_range_set_value_sett :public rw_range_set_value_sett
You can’t perform that action at this time.
0 commit comments