[klee-dev] Current status of Z3 with FP-support

[Dan Liew]

Hi,

On 12 June 2017 at 13:12, Henrik Tjäder <henrik at tjaders.com> wrote:
> Hi,
>
> Reading (1) and quoting Dan Liew,
>
> "I'm aware of klee-fp. However I should warn you (so that you don't
> waste time doing this) that I (and another research institution) have
> already extended KLEE with floating point support using Z3. We intend
> to open source our implementations in the very near future."
>
> I am curious about the state of this ongoing work, and if there are any
> need for testers or such.

Just to note my fork of KLEE that supports floating point arithmetic
is now open source [1].
You can build it is as normal but you

* Have to build using CMake
* You have to build with Z3 support and use that as the constraint solver.

The intention is to eventually upstream this implementation along with
the implementation
of one of my collaborators [2]. It will be several months before this
happens though.

Have fun,
Dan

[1] https://github.com/srg-imperial/klee-float
[2] https://github.com/danielschemmel/klee-z3float-aachen