Mus computation does not work when input file contains duplicated contiguous clauses (aka MUS competition bug)
During the SAT 2011 competition MUS track, Sat4j MUS was found incorrect (i.e. the solution found was not an UNSAT core).
Those instances do contain unit clauses, so it is probably the case that Sat4j MUS does not output the unit clauses in the solution line because unit clauses are handled specifically in the solver.
That issue should not be difficult to handle. Incorrect answers were found on the following benchmarks:
mus/marques-silva/product-configuration/C168_FW_UT_851.cnf mus/marques-silva/design-debugging/c5315-bug-gate-0.dimacs.seq.filtered.cnf mus/marques-silva/design-debugging/c7552-bug-gate-0.dimacs.seq.filtered.cnf mus/marques-silva/equivalence-checking/c2670.cnf