alt Hacker NewsI love z3. I used it for the first time for Jane Street's puzzle last year involving a hashing alg disguised as a neural network. I use a lot of MCMC at work and I have made a few small investigations into MCMC model formal verification via z3, but nothing real yet. This has inspired me to pick that back up.
Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.