https://bugzilla.redhat.com/show_bug.cgi?id=2223012
Bug ID: 2223012
Summary: Review Request: cvc5 - Automatic theorem prover for
SMT problems
Product: Fedora
Version: rawhide
Hardware: All
OS: Linux
Status: NEW
Component: Package Review
Severity: medium
Priority: medium
Assignee: nobody(a)fedoraproject.org
Reporter: loganjerry(a)gmail.com
QA Contact: extras-qa(a)fedoraproject.org
CC: package-review(a)lists.fedoraproject.org
Target Milestone: ---
Classification: Fedora
Spec URL:
https://jjames.fedorapeople.org/cvc5/cvc5.spec
SRPM URL:
https://jjames.fedorapeople.org/cvc5/cvc5-1.0.5-1.fc39.src.rpm
Fedora Account System Username: jjames
Description: This package is intended to replace the cvc4 package currently in
Fedora. However, some other packages (drat-trim, lfsc, libpoly, symfpu, and
cadical) need to be updated to support cvc5. Just to make things fun, those
same updates break cvc4, so I cannot push them to Rawhide until cvc5 has been
added, at which point cvc4 will be retired.
To make it possible to test and review cvc5, I have created a COPR that
contains the necessary package updates:
https://copr.fedorainfracloud.org/coprs/jjames/CVC5/
Package description follows:
CVC5 is a tool for determining the satisfiability of a first order formula
modulo a first order theory (or a combination of such theories). It is the
fifth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3,
CVC4) but does not directly incorporate code from any previous version prior to
CVC4.
CVC5 is intended to be an open and extensible SMT engine. It can be used as a
stand-alone tool or as a library. It has been designed to increase the
performance and reduce the memory overhead of its predecessors.
--
You are receiving this mail because:
You are on the CC list for the bug.
You are always notified about changes to this product and component
https://bugzilla.redhat.com/show_bug.cgi?id=2223012
Report this comment as SPAM:
https://bugzilla.redhat.com/enter_bug.cgi?product=Bugzilla&format=rep...