Bug: A project should not contain unreachable code.

[ustchcs-bugfinder]

z3/src/smt/theory_pb.cpp

Line 1369 in 8439057

return z*10 >= nz;

       for (unsigned i = 0; i < lemmas.size(); ++i) {
            clause* cl = lemmas[i];
            if (!cl->deleted()) {
                for (literal lit : *cl) {
                    if (m_occs.contains(lit.var())) {
                        break;
                    }
                }
            }
        }

        //std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
        return z*10 >= nz;   // The code next line will not be reached. There is no comment for why returning here.

        m_occs.reset();
        for (unsigned i = 0; i < lemmas.size(); ++i) {
            clause* cl = lemmas[i];
            unsigned sz = cl->get_num_literals();
            for (unsigned j = 0; j < sz; ++j) {
                unsigned idx = cl->get_literal(j).index();
                m_occs.insert(idx);
            }
        }
    }

This kind of problems are too many. It looks very causal to add return or throw statements without a /*TODO*/ or /*FIXME*/ comment to let others know what happened.

https://github.com/Z3Prover/z3/blob/master/src/ast/datatype_decl_plugin.cpp#L647
https://github.com/Z3Prover/z3/blob/master/src/ast/fpa/fpa2bv_converter.cpp#L1174
...

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-1.1: A project should not contain unreachable code.)

[NikolajBjorner]

Not sure where the ... are, but non-... references have if 0 guards or otherwise