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

[Christoph Wintersteiger]

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?

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/people/cwinter/


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Delcypher
Sent: 08 October 2016 11:44
To: smt-lib <smt-lib at cs.nyu.edu>
Subject: [SMT-LIB] A theory for quantifier free theory for arrays of floating point numbers and bitvectors

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.