Don't try to make inexpressable assertions
Don't try to make inexpressable assertions

This was producing an assertion that the return value of sparticus was
less than a number greater than it's return bitwidth could express. Z3's
response to being given this number (_ bv4 2) is to return unsat,
always. Which isn't unreasonable.

Get around this by detecting this condition and exiting early.

jmorse/numbness