For better or worse, it's not that uncommon for licenses to complicate it. To take one prominent example, Microsoft Research's Z3 is completely proprietary: source-code is available but you cannot make any derivative works of it (except in-house without distribution). The famous Q array-processing language is also completely proprietary. Less restrictively, it's common for things to be released under an "academic use only" or "noncommercial use only" license.

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.