Bug: a break statement is missing (very likely)

[ustchcs-bugfinder]

z3/src/math/lp/nla_core.cpp

Line 1864 in 7fc4653

k = 4;

switch (m_lar_solver.get_column_type(j)) {
        
    case lp::column_type::fixed:
        k = 0;
        break;
    case lp::column_type::boxed:
        k = 2;
        break;
    case lp::column_type::lower_bound:
    case lp::column_type::upper_bound:
        k = 4;                                             // break is MISSING?
    case lp::column_type::free_column:
        k = 6;
        break;
    default:
        UNREACHABLE();
        break;
    }

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-9.3: Each non-empty case of switch statement should be ended with an unconditional break, throw or return statement.)