[NotableAlamode]

Idris and Coq are based on the Curry-Howard correspondence. That makes it difficult / impossible to integrate Z3, because Z3 in general does not output concrete proofs. More precisely, some Z3 modules can output proof objects, but not all. There is work on integrating Z3 with LCF-style provers like Isabelle [1]. There is also active work on Z3 integration with Coq, although I'm not sure how this works. See [2] for a brief discussion of these issues by one of the Z3 authors.

[1] http://www21.in.tum.de/~boehmes/proofrec.pdf

[2] http://stackoverflow.com/questions/11531589/difference-betwe...

[Eridrus]

Are there actually cases where Z3 will say sat, but not output a model when you ask for it?

I haven't run into that issue myself, but I've mostly written toy code for it.

[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.