[RFC] Make conversion failures in the propositional back-end fatal [depends-on: #6914, #6915]

[tautschnig]

With the exception of some uses of quantifiers that should not be any
cases left that are unsupported by the back-end (while generated by a
sane front-end).

I'm marking this as RFC as I may well be missing something, and the incomplete quantifier support could be a blocker for some users.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[peterschrammel]

👍 from me, having fallen into this trap myself several times.

[martin-cs]

In principle ... yes... ish...

1. The current state-of-affairs where the user has to check for a particular "warning" or risk incorrect results is wrong and needs to be changed. Like @peterschrammel I have also run into this "in the wild".
2. A fatal error removes the risk and so is An Improvement.
3. Do we know of valid user inputs that can trigger this? If so then it should probably be a throw. If there are no known ways of triggering it then an invariant, although I do wonder if UNIMPLEMENTED or UNHANDLED_CASE would be better.

This feels a bit like the discussion about "unsafe" options #6480 . So it would sort of be nice to do something that works with that. This should only ever over-approximate the set of models, right? So it would be, in principle, OK to return proofs? It's C/E's that are suspect? I don't think this needs to be in this PR but it is another angle / use-case / things to think about for anyone working on #6480.

[martin-cs]

Approve but please consider the comments about throw vs. invariant and what flavour of invariant. It is fine if the consideration does not change the code.

[tautschnig]

A first problem to resolve before making progress on this one is #6914.

[tautschnig]

The second problem is addressed by #6915.

[tautschnig]

Note to self: we should also audit all the explicit uses of throw in solvers/flattening.