Integer proof dumps to shell when an unsupported SMT solver used.

[weaversa]

Cryptol> :prove \(x:integer) -> x+x+(toInteger 16) == x*(toInteger 2)
[warning] at <interactive>:1:1--1:54:
  Defaulting type parameter 'bits'
             of literal or demoted expression
             at <interactive>:1:32--1:34
  to 5
[warning] at <interactive>:1:1--1:54:
  Defaulting type parameter 'bits'
             of literal or demoted expression
             at <interactive>:1:52--1:53
  to 2
cryptol: SBV: Given problem needs unbounded integers
*** Which is not supported by SBV for the chosen solver: ABC

CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMTLib.hs:55:32 in sbv-7.1-9aUXGl40BzlCBvo7awIGEy:Data.SBV.SMT.SMTLib

[brianhuffman]

Apparently there a bunch of places where the SBV library will call the Haskell error function when something goes wrong, causing cryptol to exit. Here's another one, where you attempt to use a prover that's not installed:

Cryptol> :set prover=boolector
Warning: boolector installation not found
Cryptol> :prove True
cryptol: Unable to locate executable for Boolector
Executable specified: "boolector"

CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMT.hs:486:23 in sbv-7.1-GWUBwRjB6reL6wJl5cixpT:Data.SBV.SMT.SMT

Apparently we need to write a handler (in the IO monad) that can catch these error calls.