Panic while compiling `libm`

[Zeta611]

Panic while compiling `libm`

[Zeta611]

I'm not really sure the above fix is the right way---at least it fixed the above issue, which happened while analyzing sqrt(https://github.com/rust-lang/libm/blob/cb2ffdf5435d3302c97a27c8ce7de48e214de037/src/math/sqrt.rs#L151).
MIRAI tried to compute transmute(old(param_1): F64, U64) / two^32 in numeric_shr, but lf was false although it was transmuted to U64.

However, MIRAI panics shortly after making more progress while analyzing the fma function(https://github.com/rust-lang/libm/blob/cb2ffdf5435d3302c97a27c8ce7de48e214de037/src/math/fma.rs#L44).

[Zeta611]

The issue while analyzing the fma function boils down to calling bv_cast with the result of bv_overflows.

bv_cast expects ast and mask to have same sorts, as it calls Z3_mk_bvand(_, ast, mask)(https://github.com/prove-rs/z3.rs/blob/26ddf7fb90ea62509bb235286024fc7f76319591/z3-sys/src/lib.rs#L2467).
However, if ast gets returned from bv_overflows, it has Boolean sort, due to the call to Z3_mk_not (https://github.com/prove-rs/z3.rs/blob/26ddf7fb90ea62509bb235286024fc7f76319591/z3-sys/src/lib.rs#L2285).
mask has BitVector sort.

The following is what happens:

get_as_bv_z3_ast(self: "Z3Solver",expression: (overflows((local_22(11): U64) - (local_20(11): U64))) as U64,num_bits: 64)
bv_cast(self: "Z3Solver",expression: overflows((local_22(11): U64) - (local_20(11): U64)),target_type: U64,num_bits: 64)
ast "(not (bvule |local_20(11)| |local_22(11)|))" has sort "Bool"
mask "#xffffffffffffffff" has sort "(_ BitVec 64)"
Error: operator is applied to arguments of the wrong sort

Not quite sure how to fix this though.

[Zeta611]

I have created a PR that fixes these issues.