Bug: variables should be initialized before using.

[ustchcs-bugfinder]

z3/src/math/lp/int_solver.cpp

Line 529 in 558233d

if (inf_l && inf_u) {

inf_l is declared but not intialized on line 523.

If the function call get_freedom_interval_for_column() returns early on line 323, inf_l will not be intialized.

So, on line 529, inf_l holds garbage value.

bool int_solver::shift_var(unsigned j, unsigned range) {
    if (is_fixed(j) || is_base(j))
        return false;
       
    bool inf_l, inf_u;                                                                       //inf_l is NOT intialized
    impq l, u;
    mpq m;
    get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);        // could return with inf_l not intialized 
    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) {                                                                  // inf_l holds garbage value
        impq new_val = m * impq(random() % (range + 1)) + x;
        lra.set_value_for_nbasic_column(j, new_val);
        return true;
    }
...

// could return with inf_l not intialized if lrac.m_r_heading[j] >= 0 holds.

bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
    if (lrac.m_r_heading[j] >= 0) // the basic var 
        return false;
   ...

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-3.2: Variables should be initialized before using..)