Reason: its function is similar to package [z3](https://dev.getsol.us/source/z3/), a theorem prover for satisfiability modulo theories (SMT) problems. However, it contains libraries and modules that z3 doesn't have. I am planning to use cvc4, along with z3, to build [solidity](https://soliditylang.org/), a programming language for developing Ethereum smart contracts.
Open source: yes, BSD-3-Clause
Latest version: https://github.com/CVC4/CVC4-archived/archive/refs/tags/1.8.tar.gz
I have already packaged it myself, but am not sure how to submit it for review, so I guess I'll put it here.
Also, this package probably does not need maintainers as it is the last version, though I am glad to be if needed.