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.
Hello,
I am playing with the recent KLEE-MultiSolver, due to H. Palikareva and C.
Cadar, trying to generate test inputs for floating point programs. I have
just successfully installed the nice tool, with Z3 as well as a couple of
other solvers enabled. My intention is to use KLEE+Z3, in which
