fix #4640

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 17, 2020 · c13e3ce · c13e3ce
1 parent df8b14d
commit c13e3ce
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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) {