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.
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.
I can resolve it (as 78.46.87.164) with Google's DNS, but then I'm getting ERR_ADDRESS_UNREACHABLE instead... Somewhere on the interwebs there must be some mighty strange routing:
$ traceroute 78.46.87.164
traceroute to 78.46.87.164 (78.46.87.164), 64 hops max, 52 byte packets
1 192.168.1.1 (192.168.1.1) 1.238 ms 1.078 ms 1.066 ms
2 46-236-104-1.customer.t3.se (46.236.104.1) 3.896 ms 1.577 ms 1.317 ms
3 46.236.64.69 (46.236.64.69) 5.090 ms 5.281 ms 2.261 ms
4 46.236.64.69 (46.236.64.69) 1.560 ms !H * 3.568 ms !H
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.