Dead code in nla_basics_lemmas.cpp

[sashakir]

 lpvar u = null_lpvar, v = null_lpvar; //Here u == null_lpvar
    bool all_int = true;
    for (auto fc : f) {
        lpvar j = var(fc);
        all_int &= c().var_is_int(j);        
        if (j == null_lpvar && abs(val(j)) == abs_mv && 
            c().vars_are_equiv(j, mon_var) &&
            (mon_var_is_sep_from_zero ||  c().var_is_separated_from_zero(j))) 
            u = j; // Here u is reassigned to null_lpvar, since j == null_lpvar in if condition
        else if (abs(val(j)) != rational(1)) 
            v = j;
    }
    if (u == null_lpvar || v == null_lpvar) //This condition is always true
        return false;    

   // The subsequent code is non-reachable 

[NikolajBjorner]

The test j == null_lpvar should have been u == null_lpvar.
So this lemma never triggered. The fix should be tested against QF_NIA.