> 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. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
