Trivial UNSAT instances do not produce 0 models

[cernoch]

If the input CNF contains a trivial contradiction (say clauses 1 and -1), sharpSAT does not calculate the number of models as 0.

See a provided test case integration/unsat-most-trivial in bbbd0b5 for reproducibility.

What I've noticed:

• Adding a binary clause on top of the trivial contradiction, the issue remains (see integration/unsat-trivial-redundant).
• If the contradiction is inferred by unit propagation, the issue is not there (see integration/unsat-by-unit-propagation).
• If the contradiction is inferred by other means, the issue is not there (see integration/unsat-exhaustive-binary).

[cernoch]

This causes the problem:

sharpSAT/include/sharpSAT/instance.h

Line 267 in 3a48aba

assert(!isUnitClause(literals[0].neg()));

At least, this should be turned into an exception, so that rhe release mode does not (silently) produce wrong results.