Comment by jeremysalwen

I'm suspicious of the theorem proving example. I thought Z3 could fail to return sat or unsat, but he is assuming that if it's not sat the theorem must be proven