When solving PMaxSAT problems, if there is no soft clause, the method isSatisfiable() works fine, i.e. it returns true, but the method model() throws a IllegalStateException even if there is a solution. I thought that the MaxSAT solver would behave exactly like MiniSATSolver when there is no soft clause but seems not.
Moreover, the ModelIterator is used to iterate over models obtained from any SAT (e.g. MiniSAT or MaxSAT) solver. I think this requires a special attention in the case of MaxSAT solving...
I attached an automatically generated CNF file for testing purposes although it seems easy to regenerate the problem.