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

[Delcypher]

Hi,

I was wondering if there was any interest in having another a logic
and accompanying benchmark category for QF_AFPBV (quantifier free
arrays of floating point numbers and bitvectors).

If there is interest I could contribute benchmarks for this.

For context I'm currently developing a fork of the KLEE symbolic
execution engine to support symbolic floating point arithmetic. KLEE
works with QF_ABV so naturally I also need support for floating point
sorts. My benchmarks would come from paths that KLEE explores in C
programs.

Attached is an example. Mathsat5 and Z3 really struggle with this benchmark.

Thanks,
Dan.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: x.smt2
Type: application/octet-stream
Size: 3021 bytes
Desc: not available
URL: </pipermail/smt-lib/attachments/20161008/d8b6692c/attachment.obj>