Is Z3 able to produce proofs for these problems? Or does it only say "unsat" and you need to trust it?