Oh, it's still missing cbmc or Saturn, which are IMHO the easiest way to translate C problems to SMT problems, because it translates the symbolic C problem automatically.<p>klee still has weird installation issues and a weird syntax, and with z3, coq, akka, agda, HOL, Isabelle and the other prover frameworks you have do it manually. I'd rather use the decade old lisp tools than learning ML or their odd syntax.