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
91
91
const_iterator end () const { return data.end (); }
92
92
const_iterator cend () const { return data.end (); }
93
93
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)); }
96
96
};
97
97
98
98
class array_exprt ;
@@ -304,8 +304,15 @@ class guarded_range_domaint:public range_domain_baset
304
304
const_iterator end () const { return data.end (); }
305
305
const_iterator cend () const { return data.end (); }
306
306
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
+ }
309
316
};
310
317
311
318
class rw_guarded_range_set_value_sett :public rw_range_set_value_sett
You can’t perform that action at this time.
0 commit comments