Bug: a break statement is missing (very likely)

[ustchcs-bugfinder]

z3/src/smt/smt_internalizer.cpp

Line 1417 in 558233d

}

 case 0:
            if (j && !j->in_region())
                m_justifications.push_back(j);
            TRACE("mk_clause", tout << "empty clause... setting conflict\n";);
            set_conflict(j == nullptr ? b_justification::mk_axiom() : b_justification(j));
            SASSERT(inconsistent());
            return nullptr;
        case 1:
            if (j && !j->in_region())
                m_justifications.push_back(j);
            assign(lits[0], j);
            inc_ref(lits[0]);
            return nullptr;
        case 2:
            if (use_binary_clause_opt(lits[0], lits[1], lemma)) {
                literal l1 = lits[0];
                literal l2 = lits[1];
                inc_ref(l1);
                inc_ref(l2);
                m_watches[(~l1).index()].insert_literal(l2);
                m_watches[(~l2).index()].insert_literal(l1);
                if (get_assignment(l2) == l_false) {
                    assign(l1, b_justification(~l2));
                }
                m_clause_proof.add(l1, l2, k, j);
                m_stats.m_num_mk_bin_clause++;
                return nullptr;
            }                                                        // break?? or fall-through???
        default: {
            m_stats.m_num_mk_clause++;

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.)