diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index bd4fd772f31..109144adb12 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -519,10 +519,10 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
     if (is_fixed(j) || is_base(j))
         return false;
        
-    bool inf_l, inf_u;
+    bool inf_l = false, inf_u = false;
     impq l, u;
     mpq m;
-    get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
+    VERIFY(get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m));
     const impq & x = get_value(j);
     // x, the value of j column, might be shifted on a multiple of m
     if (inf_l && inf_u) {