If researcher found satisfiability in any software, this is a threat to security? If answer - "Yes", how can attacker to use SAT?
The symbolic execution technique, as used in KLEE, is just a way to ask a SAT-solver to validate/invalidate possible runs in the software without executing it for real. It allows to focus on feasible paths only.
So, this will not be a security threat if you can run a SAT-solver and validate/invalidate the paths of your software. I will just mean that you will be able to explore all its execution paths for sure (exhaustively).
It also means that the internal of your software can be fully explored, which might be a problem if you want to hide something (a patented algorithm, a cryptographic key, ...). In such case, people tends to use specific obfuscation techniques (usually specific opaque predicates to defeat SAT-solvers) to render the exploration of all the executable paths more difficult.
Hope this help you to better understand the whole thing.