[psuter]

Models are not proofs (in fact they're the opposite). In SAT/SMT, a proof is a sequence (a tree really) of deductions that show that you can conclude "false" from the set of initial assumptions, and that, therefore, there is no model.

[NotableAlamode]

I'm not sure I understand what you are saying here.

The tree of resolution deductions that SAT provers (modulo theories or otherwise) like Z3 produce is of course a proof in a valid proof system. Typically that is some variant of a propositional resolution proof system. The problem is that the reasoning is classical: to show A, falsity is deduced from (not A). This is not constructively valid, you can only deduce (not not A) if (not A) implies falsity.

So the resolution proof that Z3 outputs can be converted to a classical proof and expressed in classical proof systems like (Isabelle/)HOL, but not in constructive systems like Coq and Agda.

[psuter]

Either I misread the parent's question or (s)he edited it. I had read it as "[...] cases where Z3 will say sat, but not output a proof when you ask for it", and was simply trying to clear up the misunderstanding that a 'sat' answer should come with a proof.