Page MenuHomeSolus

Closed, WontfixPublic


Name: cvc4
Reason: its function is similar to package 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, a programming language for developing Ethereum smart contracts.
Open source: yes, BSD-3-Clause
Latest version:

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.
Even though cvc5 is the newest version, it is still in prerelease. Hence, the newest stable version for now is the just-archived cvc4 version 1.8

Event Timeline

GZGavinZhao updated the task description. (Show Details)May 7 2021, 9:27 PM
GZGavinZhao updated the task description. (Show Details)May 7 2021, 9:54 PM
DataDrake closed this task as Wontfix.May 7 2021, 11:00 PM
DataDrake added a subscriber: DataDrake.

Per the discussion on IRC, cvc4 is EOL in favor of cvc5. We don't want to add a package only to turn around and deprecate it, so I'd rather wait until cvc5 is available. You can request that, but it will get marked Awaiting Package Upgrades and won't be eligible for inclusion until it is stable.