[klee-dev] KLEE+Z3 (an instance of KLEE-MultiSolver) still concretizes floating point expression to 0.

[Dan Liew]

> Is there a way to tell KLEE not to concretieze floating point expression to
> 0 so KLEE + Z3 can be useful when handling floating point program?
>

Not right now no. KLEE's expression language does not support floating
point constraints right now which is why floating point numbers get
concretised. There is a fork of KLEE (KLEE-CL/KLEE-FP) that does
support floating point numbers in its expression language (but not for
constraint solving via an SMT solver) but it is not actively
maintained.