And the papers I've read about array languages don't base their languages on Q. I haven't done much reading on theorem provers, but I suspect I'll see a lot more papers about things derived from ACL2 or Coq than from Z3.