From c13e3ce693e9a57a16d747b1fec40fd46d20b8d9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 17 Aug 2020 08:38:07 -0700
Subject: [PATCH] fix #4640

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/int_solver.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index bd4fd772f..109144adb 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) {