Skip to content

Commit dd83fb9

Browse files
committed
Use random_shuffle in a future-proof way
Variants of random_shuffle supported in C++11 have been deprecated in later versions of the standard. Specifying a random-number generator is supported as of C++11 and not (yet) deprecated in any later version.
1 parent 9822b27 commit dd83fb9

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

unit/util/interval/get_extreme.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@
1313
#include <util/simplify_expr.h>
1414
#include <util/symbol_table.h>
1515

16+
#include <random>
17+
1618
#define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true))
1719
#define V_(X) (bvrep2integer(X.c_str(), 32, true))
1820
#define CEV(X) (from_integer(mp_integer(X), signedbv_typet(32)))
@@ -147,7 +149,9 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]")
147149

148150
WHEN("All from [-100:100] are shuffled and selected")
149151
{
150-
std::random_shuffle(ve.begin(), ve.end());
152+
std::random_device rd;
153+
std::mt19937 g(rd());
154+
std::shuffle(ve.begin(), ve.end(), g);
151155

152156
exprt min = constant_interval_exprt::get_extreme(ve, true);
153157
exprt max = constant_interval_exprt::get_extreme(ve, false);

0 commit comments

Comments
 (0)