From fd3c3a2599872c155175cd82a63e97746509aee4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 9 Feb 2020 16:30:09 -0800 Subject: [PATCH] make the column shift in random_update divisible by m Signed-off-by: Lev Nachmanson --- src/math/lp/int_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 3a718a3f4..b9ceaa1ae 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -517,7 +517,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) { // the interval contains at least range multiples of m. // the number of multiples to the left of the value of j is floor((get_value(j) - l.x)/m) // shift either left or right of the current value by available multiples. - impq shift = impq(random() % (range + 1)) - impq(floor(x.x - l.x) / m); + impq shift = impq(random() % (range + 1)) - impq(floor((x.x - l.x) / m)); impq new_val = x + m * shift; SASSERT(l <= new_val && new_val <= u); set_value_for_nbasic_column_ignore_old_values(j, new_val); return true;