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

Delcypher delcypher at gmail.com
Mon Oct 10 14:49:49 EDT 2016


Hi Christoph,

On 10 October 2016 at 11:50, Christoph Wintersteiger
<cwinter at microsoft.com> wrote:
> Hi all,
>
> Absolutely, we're definitely interested in your benchmarks! I currently manage BV and FP, and I'm happy to take care of this new logic too.
>
> I suppose they are too large to send by email; do you have a place to put them so that I can access them?

I don't currently have many solver queries collected but I will gather
them when I have finished performing the evaluation of my fork which
will probably be done in the next few months. This e-mail was just to
gauge interest and I'm glad to see there is some.

Is there any particular deadline for submitting benchmarks?

Thanks,
Dan Liew.


More information about the SMT-LIB mailing list