Allow some solvers to fail when using prover=any

[atomb]

Right now, if any of the provers invoked using prover=any fails, Cryptol quits. It would be more convenient to just ignore (and maybe mention) any prover crashes, and simply report the result of the first successful prover. See also #436.

[jpziegler]

Now that we have a bunch of new types in Cryptol, this also crops up when a solver doesn't support a particular theory:

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.7.1 (2ce982a, modified)

Loading module Cryptol
Cryptol> :s prover=any
Cryptol> :sat \(x,y) -> x*y == (2147483647:Integer) /\ x > 1 /\ y > 1

SBV error:
SBV: Given problem needs unbounded integers
*** Which is not supported by SBV for the chosen solver: Boolector

Note that most of the solvers don't support this theory; it just happens to choose Boolector to complain about. (I was running with all 6 solvers available.)

[atomb]

Let's see if we can make this work better with What4.

[brianhuffman]

If this is a problem with SBV, then we should open a ticket on the SBV repository.

[robdockins]

Did we open an SBV ticket for this?

[robdockins]

Fixed via #788.