[klee-dev] silently concretize float expression to value

[Cristian Cadar]

>> I want to work with examples that has float. Can KLEE deal with this?
>
> KLEE cannot currently handle symbolic floating point expressions. A
> fork KLEE called KLEE-FP can handle symbolic floating point
> expressions. See http://www.pcc.me.uk/~peter/klee-fp/

Just a quick clarification: KLEE-FP has support for floating point only 
in the context of reasoning about code equivalence.  See our paper for 
more details: http://www.doc.ic.ac.uk/~cristic/papers/kleefp-eurosys-11.pdf

Best,
Cristian