I haven't understood from the articles, sorry
but is Z3 sound?
It should be unless there is a bug.
If we answer "unsat" then the formula is really unsatisfiable. (the negation of the formula is valid).Answering "sat" should mean that the formula really is satisfiable. Otherwise, we should answer "unknown".
Nikolaj, thank you!
By the way, are there any issued papers / reports / books / ppts
stating that Z3 is sound?
I use Z3 in my phd studies and need some references to prove almost each statement. References for Z3 are especially needed for there are papers about ESC / Java stating that it is neither complete nor sound, and - on the other hand - papers about ACL2 or Key stating soundness...
So I'm always asked - wheather the verifier I'm using is sound
I see the context: for ESC/Java soundness means something different. In the context of ESC/Java the input to the tool is a program and a specification in the form of freedom from runtime errors and possibly also a specification that some pre-post conditions or object invariants hold. As far as I recall, soundness is there used by Greg and Rustan and others as meaning that all possible runtime errors are caught.
The context of Z3 is first-order logic not program verification, it addresses what it means to check formulas for satisfiability (or dually prove theorems).Soundness in this context is that only theorems are provable (dually only unsatisfiable formulas are flagged as unsatisfiable), and furthermore, if we say a formula is satisfiable, then indeed it is satisfiable (and not mistakingly unsatisfiable).When we deal with theories that are decidable, we can in these cases know for sure (unless timing out or running out of resources)whether a formula is unsatisfiable or satisfiable.Theorem provers, including Z3, should in general always be sound. Unsoundness (that is, deriving non-theorems) should always be considered a bug.The terminology from ESC/Java tends to be somewhat confusing in this context.
Now it's clear.
Nikolaj, thank you very much