Z3 is a contraint solver (SMT, SAT) which makes total sense to use in a design by contract system, but AFAIK there is zero link to abstract interpretation (which from what I understood about it, is way harder to use).
How else are you going to check the contracts at compile time?
I honestly don't know if that's how DrNim works or if there are other ways to achieve that.
But a similar tool for Python does it exactly this way:
https://github.com/pschanely/CrossHair
"CrossHair works by repeatedly calling your functions with symbolic inputs. It uses an SMT solver (a kind of theorem prover) to explore viable execution paths and find counterexamples for you."
...so that's where I got the idea that DrNim is probably doing the same
It's talking about DrNim, and docs page for that https://nim-lang.org/docs/drnim.html says:
"DrNim combines the Nim frontend with the Z3 proof engine in order to allow verify / validate software written in Nim"
So I think the design-by-contract annotations are being checked via abstract interpretation (that's what gets fed into Z3 I think?)