{"bugs":[{"bugid":895770,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/stp-2.3.3-r2 help2man: can't get `--help' info from \/var\/tmp\/portage\/sci-mathematics\/stp-2.3.3-r2\/work\/stp-2.3.3_build\/stp"},{"bugid":942340,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/stp-2.3.4 fails tests: 9 - StrengthReduction_TestTests-gtest (Subprocess aborted)"},{"bugid":957437,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/stp-2.3.4 - QA Notice: Compatibility with CMake < 3.5 has been removed from CMake 4,"}],"categories":[{"categoryid":452,"name":"dev-db","summary":"The dev-db category contains libraries and utilities for database related programming."},{"categoryid":450,"name":"dev-lang","summary":"The dev-lang category contains various programming language implementations and related tools."},{"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."},{"categoryid":396,"name":"virtual","summary":"The virtual category contains packages which satisfy virtual dependencies."}],"changelog":[{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"5a1adb610b1d91ab6683cbe671e266f424224c16","committime":"2025-11-04T08:35:48","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"mgorny@gentoo.org","authorname":"Michał Górny","body":"Update done using:\n\n```\ngit grep -l sys-libs\/zlib dev-* | xargs sed -i -e s@sys-libs\/zlib@virtual\/zlib@g\ngit diff --name-only | xargs copybump\ngit diff --name-only | xargs grep -l PYTHON_COMPAT | xargs gpy-impl -@dead\npkgcheck scan --commits -c SourcingCheck,VisibilityCheck --exit error\n```\n\nSigned-off-by: Michał Górny ","commitid":"f1351833569f8b22abc3dc9e74abeed7e8641096","committime":"2025-11-04T08:17:06","packageid":73915,"repoid":1,"summary":"sci-*\/*: update for virtual\/zlib"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"59e00f91407127298e125e8ce46064ede0c72196","committime":"2024-11-22T21:48:18","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"mgorny@gentoo.org","authorname":"Michał Górny","body":"Signed-off-by: Michał Górny ","commitid":"1cb7588b512b2e5e56d438fd5a7cdb748fa662c3","committime":"2024-11-22T21:18:20","packageid":73915,"repoid":1,"summary":"Rename dev-python\/{OutputCheck → outputcheck}"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"9736749844c79c616b8a06f6de81d0c8f6625c3d","committime":"2024-06-28T23:35:47","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/880135\nSigned-off-by: Maciej Barć ","commitid":"57c9698e1ddecc9a6bd97d304d9da851e4c9d158","committime":"2024-06-28T23:26:28","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: build tweaks"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0f54615c9ebe139b7a3b4598bc8383effffbeac9","committime":"2024-06-27T22:48:56","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"e30f1a8f185d708ad0b29cac597dc195a7c2d064","committime":"2024-06-27T22:39:22","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: bump to 2.3.4"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"e32fc1c529e3f48c432ff4d3e8f4b17922383770","committime":"2024-04-29T19:04:10","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/929798\nSigned-off-by: Maciej Barć ","commitid":"351b0d97c04df35ea8b9f1e70db4f4295f2b5afc","committime":"2024-04-29T17:08:55","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: enable py3.12 compat"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"efe3d02cd6e19168c55ddc0b8c094f2645cbe233","committime":"2023-02-22T00:01:56","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"335dfafb43cfb8574492617237712bcc324e980c","committime":"2023-02-21T22:22:14","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: update PYTHON_COMPAT; add help2man to BDEPEND"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"b003ec5b8f02ed5d3f92eb18e2f84852fde5a154","committime":"2023-02-20T01:01:54","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/895096\nSigned-off-by: Maciej Barć ","commitid":"c7aee643a9472d7ea97c8e1266ed8102e3298535","committime":"2023-02-20T00:32:10","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: patch - include cstdint"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"337f35c9db81b2c00da792a1596d8d4aec2d0509","committime":"2023-02-20T00:20:17","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: rename patches"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"8d0ebee607de5c63d747980fbeb0806c193a29c9","committime":"2023-01-14T13:02:17","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"soap@gentoo.org","authorname":"David Seifert","body":"Signed-off-by: David Seifert ","commitid":"ed468028e725c9580a7b2ee02d6b7b9375f7a0b2","committime":"2023-01-14T12:51:19","packageid":73915,"repoid":1,"summary":"*\/*: remove py3.8 from PYTHON_COMPAT"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"7c931621bb3ef4f25157a98d317d6713aafd3b20","committime":"2022-11-06T20:16:44","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/879325\nSigned-off-by: Maciej Barć ","commitid":"d1f7a354dc856bde7a58abfe3d4c5f2cff71ccfa","committime":"2022-11-06T20:09:52","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: do not run C API tests"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"8c5457158be0f674d45de99103d9f3d7a67d06ab","committime":"2022-08-08T21:01:48","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/864124\nSigned-off-by: Maciej Barć ","commitid":"b7c9de657e647f16a7f16c9aae0ba76fb9011312","committime":"2022-08-08T20:33:54","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: compile python modules"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"a3b322565d357d546480ba8bf27f2ceea273465e","committime":"2022-08-07T00:01:55","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/863263\nSigned-off-by: Maciej Barć ","commitid":"75cac060d43476807e769eb8f21dfeeb2c54d721","committime":"2022-08-06T23:48:15","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: filter LTO (ODR)"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0fdc51113d494a0a5b44d1313852ba1c985f502c","committime":"2021-12-27T13:21:39","packageid":73915,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"- add missing test submodules\n- add optional cryptominisat dependency (USE=dependency)\n- add the Gentoo Mathematics Project to co-maintainers\n- change python to optional dependency (USE=python)\n- install PDF documentation\n- patch CMakeLists.txt to fix CFLAGS\n- patch stp.py to fix python module\n\nCloses: https:\/\/bugs.gentoo.org\/759457\nPackage-Manager: Portage-3.0.28, Repoman-3.0.3\nSigned-off-by: Maciej Barć ","commitid":"317c9f66693a8341a07ba45fe158e8699cc1cd19","committime":"2021-12-27T13:08:03","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: multiple fixes"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"6f0b9d2bc3952de477fefeaa68783e5dc27e4e2d","committime":"2021-12-27T13:07:02","packageid":73915,"repoid":1,"summary":"sci-mathematics\/stp: dev-libs -> sci-mathematics"}],"dependencies":[{"block":false,"categoryid":450,"description":"An interpreted, interactive, object-oriented programming language","ebuildids":[778718,778718,831242,831242,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"python@gentoo.org","maintainername":"Python","name":"python","packageid":43095},{"block":false,"categoryid":393,"description":"Boost Libraries for C++","ebuildids":[778718,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"cpp@gentoo.org","maintainername":"Gentoo C++ Project","name":"boost","packageid":45155},{"block":false,"categoryid":452,"description":"SQL database engine","ebuildids":[778718,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"arfrever.fta@gmail.com","maintainername":"Arfrever Frehtes Taifersar Arahesis","name":"sqlite","packageid":50388},{"block":false,"categoryid":393,"description":"International Components for Unicode","ebuildids":[778718,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"office@gentoo.org","maintainername":"Gentoo Office project","name":"icu","packageid":54373},{"block":false,"categoryid":317,"description":"Small yet efficient SAT solver with reference paper","ebuildids":[778718,831242],"firstseen":"2011-04-10T14:39:35.202649","maintainer":"sci@gentoo.org","maintainername":"Gentoo Science Project","name":"minisat","packageid":57212,"summary":"MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. It is released under the MIT licence, and is currently used in a number of projects. MiniSat is small and well-documented, and possibly also well-designed, making it an ideal starting point for adapting SAT based techniques to domain specific problems. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting point both for future research in SAT, and for applications using SAT. MiniSat supports incremental SAT and has mechanisms for adding non-clausal constraints. By virtue of being easy to modify, it is a good choice for integrating as a backend to another tool, such as a model checker or a more generic constraint solver."},{"block":false,"categoryid":317,"description":"Advanced SAT solver with C++ and command-line interfaces","ebuildids":[778718,831242],"firstseen":"2021-12-26T20:23:15.104272","name":"cryptominisat","packageid":73913,"summary":"This system provides CryptoMiniSat, an advanced incremental SAT solver. The system has 3 interfaces: command-line, C++ library and python. The command-line interface takes a cnf as an input in the DIMACS format with the extension of XOR clauses. The C++ and python interface mimics this and also allows for incremental use: assumptions and multiple solve calls."},{"block":false,"categoryid":396,"description":"Virtual for libz.so providers","ebuildids":[778718,831242],"firstseen":"2025-11-04T07:31:41.418357","name":"zlib","packageid":78605}],"depending":[],"ebuilds":[{"archs":["~amd64","~x86"],"ebuildid":831242,"firstseen":"2024-06-28T00:00:30.342602","license":"GPL-2+ MIT","moddate":"2026-03-28T18:04:21","packageid":73915,"repoid":1,"slot":"0\/2.3.4","uses":["cryptominisat","debug","python","python_single_target_python3_11","python_single_target_python3_12","python_single_target_python3_13","test"],"version":"2.3.4"},{"archs":["~amd64","~x86"],"ebuildid":778718,"firstseen":"2023-02-22T00:09:47.608143","license":"GPL-2+ MIT","moddate":"2026-03-28T18:04:21","packageid":73915,"repoid":1,"slot":"0\/2.3.3","uses":["cryptominisat","debug","python","python_single_target_python3_11","python_single_target_python3_12","test"],"version":"2.3.3-r3"}],"masks":[],"package":{"categoryid":317,"description":"Simple Theorem Prover, an efficient SMT solver for bitvectors","firstseen":"2021-12-27T13:30:54.463898","name":"stp","packageid":73915,"summary":"STP is a constraint solver (or SMT solver) aimed at solving constraints of bitvectors and arrays. These types of constraints can be generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications."},"rdependencies":[{"block":false,"categoryid":450,"description":"An interpreted, interactive, object-oriented programming language","ebuildids":[778718,778718,831242,831242,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"python@gentoo.org","maintainername":"Python","name":"python","packageid":43095},{"block":false,"categoryid":393,"description":"Boost Libraries for C++","ebuildids":[778718,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"cpp@gentoo.org","maintainername":"Gentoo C++ Project","name":"boost","packageid":45155},{"block":false,"categoryid":452,"description":"SQL database engine","ebuildids":[778718,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"arfrever.fta@gmail.com","maintainername":"Arfrever Frehtes Taifersar Arahesis","name":"sqlite","packageid":50388},{"block":false,"categoryid":393,"description":"International Components for Unicode","ebuildids":[778718,831242],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"office@gentoo.org","maintainername":"Gentoo Office project","name":"icu","packageid":54373},{"block":false,"categoryid":317,"description":"Small yet efficient SAT solver with reference paper","ebuildids":[778718,831242],"firstseen":"2011-04-10T14:39:35.202649","maintainer":"sci@gentoo.org","maintainername":"Gentoo Science Project","name":"minisat","packageid":57212,"summary":"MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. It is released under the MIT licence, and is currently used in a number of projects. MiniSat is small and well-documented, and possibly also well-designed, making it an ideal starting point for adapting SAT based techniques to domain specific problems. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting point both for future research in SAT, and for applications using SAT. MiniSat supports incremental SAT and has mechanisms for adding non-clausal constraints. By virtue of being easy to modify, it is a good choice for integrating as a backend to another tool, such as a model checker or a more generic constraint solver."},{"block":false,"categoryid":317,"description":"Advanced SAT solver with C++ and command-line interfaces","ebuildids":[778718,831242],"firstseen":"2021-12-26T20:23:15.104272","name":"cryptominisat","packageid":73913,"summary":"This system provides CryptoMiniSat, an advanced incremental SAT solver. The system has 3 interfaces: command-line, C++ library and python. The command-line interface takes a cnf as an input in the DIMACS format with the extension of XOR clauses. The C++ and python interface mimics this and also allows for incremental use: assumptions and multiple solve calls."},{"block":false,"categoryid":396,"description":"Virtual for libz.so providers","ebuildids":[778718,831242],"firstseen":"2025-11-04T07:31:41.418357","name":"zlib","packageid":78605}],"repos":[{"branch":"master","lastcommit":"82366aa45a35f6900f43023917c2c86ccdbb00a3","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/stp\/stp\/","https:\/\/stp.github.io\/"],"uses":[{"description":"Enable sci-mathematics\/cryptominisat support","isdefault":false,"packageid":73915,"use":"cryptominisat"},{"description":"Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https:\/\/wiki.gentoo.org\/wiki\/Project:Quality_Assurance\/Backtraces","isdefault":false,"use":"debug"},{"defaultflag":true,"description":"Enable building the Python interface","isdefault":true,"packageid":73915,"use":"python"},{"description":"Enable dependencies and\/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)","isdefault":false,"use":"test"},{"description":"Build for Python 3.11 only","group":"python_single_target","isdefault":false,"use":"python3_11"},{"description":"Build for Python 3.12 only","group":"python_single_target","isdefault":false,"use":"python3_12"},{"description":"Build for Python 3.13 only","group":"python_single_target","isdefault":false,"use":"python3_13"}]}