{"bugs":[{"bugid":926436,"firstseen":"2024-03-08T10:00:25.023765","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/yices2-2.6.4-r1 fails tests"}],"categories":[{"categoryid":393,"name":"dev-libs","summary":"The dev-libs category contains various miscellaneous programming libraries."},{"categoryid":317,"name":"sci-mathematics","summary":"The sci-mathematics category contains mathematical software."}],"changelog":[{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"5f4da586bc502c85a7e5c44cdf53f19c937adb69","committime":"2023-01-14T03:02:04","packageid":75684,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/890758\nSigned-off-by: Maciej Barć <xgqt@gentoo.org>","commitid":"d7f3217ec85f5d56436c755de99b5c1938c3f547","committime":"2023-01-14T02:24:15","packageid":75684,"repoid":1,"summary":"sci-mathematics\/yices2: do not install static libs"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"daa6ca61d6a7d0fb6d45c5e96bdc6eb478a1fbf0","committime":"2022-12-18T22:02:14","packageid":75684,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć <xgqt@gentoo.org>","commitid":"7fedb4d85d18416471f5f7fda0aec80c15cde3eb","committime":"2022-12-18T21:41:32","packageid":75684,"repoid":1,"summary":"sci-mathematics\/yices2: new package; add 2.6.4"}],"dependencies":[{"block":false,"categoryid":393,"description":"Library for arbitrary-precision arithmetic on different type of numbers","ebuildids":[774782],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"toolchain@gentoo.org","maintainername":"Gentoo Toolchain Project","name":"gmp","packageid":55512},{"block":false,"categoryid":317,"description":"Colorado University binary Decision Diagram library","ebuildids":[774782],"firstseen":"2022-12-18T22:22:04.912741","name":"cudd","packageid":75682,"summary":"CUDD stands for Colorado University Decision Diagram. It is a package for the manipulation of Binary Decision Diagrams (BDDs), Algebraic Decision Diagrams (ADDs) and Zero-suppressed Binary Decision Diagrams (ZDDs)."},{"block":false,"categoryid":317,"description":"C library for manipulating polynomials","ebuildids":[774782],"firstseen":"2022-12-18T22:22:04.912741","name":"libpoly","packageid":75683,"summary":"LibPoly is a C library for manipulating polynomials. The target applications are symbolic reasoning engines, such as SMT solvers, that need to reason about polynomial constraints. It is research software under development, so the features and the API might change rapidly."}],"depending":[],"ebuilds":[{"archs":["~amd64","~x86"],"ebuildid":774782,"firstseen":"2023-01-14T03:04:55.321958","license":"GPL-3+","moddate":"2025-04-23T15:45:16","packageid":75684,"repoid":1,"slot":"0\/2.6.4","uses":["mcsat"],"version":"2.6.4-r1"}],"masks":[],"package":{"categoryid":317,"description":"SMT Solver supporting SMT-LIB and Yices specification language","firstseen":"2022-12-18T22:22:04.912741","name":"yices2","packageid":75684,"summary":"Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both linear and nonlinear arithmetic. Yices 2 can process input written in the SMT-LIB notation (both versions 2.0 and 1.2 are supported). Alternatively, you can write specifications using Yices 2's own specification language, which includes tuples and scalar types. You can also use Yices 2 as a library in your software."},"rdependencies":[{"block":false,"categoryid":393,"description":"Library for arbitrary-precision arithmetic on different type of numbers","ebuildids":[774782],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"toolchain@gentoo.org","maintainername":"Gentoo Toolchain Project","name":"gmp","packageid":55512},{"block":false,"categoryid":317,"description":"Colorado University binary Decision Diagram library","ebuildids":[774782],"firstseen":"2022-12-18T22:22:04.912741","name":"cudd","packageid":75682,"summary":"CUDD stands for Colorado University Decision Diagram. It is a package for the manipulation of Binary Decision Diagrams (BDDs), Algebraic Decision Diagrams (ADDs) and Zero-suppressed Binary Decision Diagrams (ZDDs)."},{"block":false,"categoryid":317,"description":"C library for manipulating polynomials","ebuildids":[774782],"firstseen":"2022-12-18T22:22:04.912741","name":"libpoly","packageid":75683,"summary":"LibPoly is a C library for manipulating polynomials. The target applications are symbolic reasoning engines, such as SMT solvers, that need to reason about polynomial constraints. It is research software under development, so the features and the API might change rapidly."}],"repos":[{"branch":"master","lastcommit":"83b1268c5aac6ae9b0760d1fb99a3cf736f62f25","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/SRI-CSL\/yices2\/"],"uses":[{"defaultflag":true,"description":"Enable support for MCSAT","isdefault":true,"packageid":75684,"use":"mcsat"}]}