mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

use random_next instead of library random

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-13 19:59:05 -07:00
parent c499bd4116
commit 90b78eb64a
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/lar_solver.cpp
View file

@ -492,7 +492,7 @@ bool lar_solver::move_non_basic_column_to_bounds(unsigned j) {
switch (lcs.m_column_types()[j]) {
case column_type::boxed:
if (val != lcs.m_r_lower_bounds()[j] && val != lcs.m_r_upper_bounds()[j]) {
if (random() % 2 == 0)
if (m_settings.random_next() % 2 == 0)
set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]);
else
set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]);