Improve error reporting

[RyanGlScott]

The error messages that copilot-verifier gives when unable to verify a program can be rather difficult to understand by non-experts. Here is one example observed in #5:

$ cabal run verify-examples -- WCV
Up to date
=====
== Running the WCV example...
=====

Generated "results/wcv/wcv.c"
Compiled wcv into results/wcv/crux~wcv.bc
Translated bitcode into Crucible
Generating proof state data
Computing initial state verification conditions
Proving initial state verification conditions
All obligations proved by concrete simplification
Computing step bisimulation verification conditions
Proving step bisimulation verification conditions
verify-examples: user error (user error (evalGroundExpr: could not evaluate expression: let uninterpreted_float_lt = ??
    uninterpreted_sbv_to_float = ??
    uninterpreted_float_to_sbv = ??
    -- results/wcv/wcv.c:21:208
    v366 = apply uninterpreted_float_to_sbv 0 crelative_velocity_x_r0@58:bv
    -- results/wcv/wcv.c:21:202
    v373 = ite (bvSlt v366 0x0:[32]) (bvSum (bvMul 0xffffffff:[32] v366)) v366
    -- results/wcv/wcv.c:21:201
    v374 = apply uninterpreted_sbv_to_float 0 v373
 in apply uninterpreted_float_lt v374 0x3f50624dd2f1a9fc:[64])
)

This was fixed by picking a different translation of abs, but it seems quite likely that there are other similarly perplexing error-message scenarios awaiting us. We should:

• Identify situations in which copilot-verifier produces dense error messages, and
• Improve the reporting of these errors so that they are more comprehensible by users who aren't experts in What4/Crucible.