[SMT-LIB] A theory for quantifier free theory for arrays of floating point numbers and bitvectors

[Delcypher]

Hi,

I'm reviving this thread because I'm now at a stage where I have the
time to start collect benchmarks. A few questions:

* Some queries may contain Z3's non standard `to_ieee_bv`. Is that a problem?
* Do I need to curate the benchmarks in any way? I can give you the
raw benchmarks or I can select a subset of the benchmarks based on
some criteria (e.g. Z3 execution time) if you prefer.
* The benchmarks do not contain the expected outcome. Is that a problem?

Thanks,
Dan.