Dear All, In KLEE, it seems symbolic floating point variables are simply converted to int and grounded to 0. I am wonderingwhat is the current state of floating point symbolic execution support in KLEE? I know there has been some workon KLEE-FP in the past, but does it actually check path feasibility via path condition satisfiability in QF_FPA?Now that KLEE supports Z3 as backend solver, perhaps such feasibility checking is not too difficult to implement?
Best, Andrew
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
