From 896925ae1c12f86aacd9dbde0de89612601fe901 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Thu, 17 Oct 2019 16:45:25 +0200 Subject: [PATCH] core: random_shuffle is deprecated and not portable * tests/core/parity.cc: Here. --- tests/core/parity.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 28689c41f..4cb8256ef 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -127,8 +127,8 @@ generate_aut(const spot::bdd_dict_ptr& current_bdd) for (auto& t: LAST_AUT->edges()) { auto nb_acc = std::rand() % (num_sets - min + 1) + min; - std::random_shuffle(cont_sets[num_sets].begin(), - cont_sets[num_sets].end()); + spot::mrandom_shuffle(cont_sets[num_sets].begin(), + cont_sets[num_sets].end()); for (auto j = 0; j < nb_acc; ++j) SET_TR(t, cont_sets[num_sets][j]); } @@ -141,8 +141,8 @@ generate_aut(const spot::bdd_dict_ptr& current_bdd) for (auto& t: LAST_AUT->edges()) { auto nb_acc = std::rand() % (num_sets - min + 1) + min; - std::random_shuffle(cont_sets[num_sets].begin(), - cont_sets[num_sets].end()); + spot::mrandom_shuffle(cont_sets[num_sets].begin(), + cont_sets[num_sets].end()); for (auto j = 0; j < nb_acc; ++j) { auto value = cont_sets[num_sets][j] * 2 + even;