{"bugs":[{"bugid":928097,"firstseen":"2024-03-29T09:04:38.844386","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/vampire-4.8 fails to compile: Portability.hpp:23:20: error: static assertion failed: Vampire assumes that the size of a pointer is 8 bytes for efficiency reasons This may be relaxed in future, but for the moment expect problems if running"},{"bugid":940574,"firstseen":"2024-10-01T07:51:31.596832","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/vampire-4.9 fails tests: 3 - UnificationWithAbstraction (Failed)"},{"bugid":942341,"firstseen":"2024-10-27T10:57:01.216583","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/vampire-4.9 fails to compile: Hash.hpp:292:51: error: uintptr_t does not name a type [-Wtemplate-body]"},{"bugid":944752,"firstseen":"2024-11-23T17:50:08.604616","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/vampire-4.9 fails to compile: Hash.hpp:291:11: error: instantiating erroneous template"},{"bugid":948184,"firstseen":"2025-01-16T10:54:48.053357","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/vampire-4.9 fails to compile: hashtable_policy.h:1491:67: error: converting to Lib::STLAllocator >, true> > from initializer list would use explicit con"}],"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":"2ac97f3c32f1451d3eaed99104678847dae5c224","committime":"2024-09-30T18:36:12","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"ea3edb5ee8118107e5cd048b9708c08cb5560027","committime":"2024-09-30T17:47:18","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: bump to 4.9"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"ee1b636d856955928ca35ccab0a70dd0567ace40","committime":"2023-08-22T14:46:34","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"15f33031b800eba31732bd4b2acd7ce659162d47","committime":"2023-08-22T14:30:18","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: drop old 4.7-r1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"2a1eaa19c8395fb76dd9a37420ade2ed0fa2cc30","committime":"2023-07-15T00:31:47","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"52bc3f379b6f9d6d2fab531cd4b6240609e231ae","committime":"2023-07-14T23:27:57","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: bump to 4.8"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"b90b274b4a0d5cdeb751b4869844510bbfcf26df","committime":"2023-07-14T22:52:09","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: drop old 4.6.1-r2"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"45e55a16bae5338b97bb8d012cbe519bccf429c6","committime":"2023-02-06T17:31:46","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Bug: https:\/\/github.com\/vprover\/vampire\/pull\/432\nCloses: https:\/\/bugs.gentoo.org\/832834\nSigned-off-by: Maciej Barć ","commitid":"d2b700163970908b03466ad2e07616c5e92623cd","committime":"2023-02-06T14:12:15","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: fix build on musl"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"bdb3bf6952fad50ed5c44ed2c49bd56bfa94bdb0","committime":"2022-09-23T11:46:40","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"both vampire 4.6.1 and 4.7 build correctly with >=sci-mathematics\/z3-4.11.2\n\nCloses: https:\/\/bugs.gentoo.org\/872512\nBug: https:\/\/bugs.gentoo.org\/860237\nSigned-off-by: Maciej Barć ","commitid":"bd70ca1e105ae6eda804d50dcb4732e1929ead74","committime":"2022-09-23T11:03:57","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: depend on z3 version >=4.11.2"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"a3b322565d357d546480ba8bf27f2ceea273465e","committime":"2022-08-07T00:01:55","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/863269\nSigned-off-by: Maciej Barć ","commitid":"c1dc1afc5592077b339f17e00e93b6bc2180f768","committime":"2022-08-06T23:50:34","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: filter LTO (strict-aliasing)"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"05007a94b1141d4c128bbf1ccda22bae4110240c","committime":"2022-07-23T17:46:33","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"09e3e38929c16b3cfde3d2ac41d780fc2c3bc9ba","committime":"2022-07-23T17:28:01","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: bump to 4.7"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/860237\nSigned-off-by: Maciej Barć ","commitid":"cbb308be9f9e203cd2a885f43e5f568fddc16cb1","committime":"2022-07-23T17:25:52","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: restrict z3 dep version"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"efd88dc4b6b9e8342980c0b91868f69f383317b9","committime":"2021-12-11T14:51:33","packageid":73738,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Package-Manager: Portage-3.0.28, Repoman-3.0.3\nSigned-off-by: Maciej Barć ","commitid":"44429a0128b114f807d95827b5eb509b065cc90f","committime":"2021-12-11T14:40:09","packageid":73738,"repoid":1,"summary":"sci-mathematics\/vampire: new package; add version 4.6.1"}],"dependencies":[{"block":false,"categoryid":393,"description":"Library for arbitrary-precision arithmetic on different type of numbers","ebuildids":[794143,839704],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"toolchain@gentoo.org","maintainername":"Gentoo Toolchain Project","name":"gmp","packageid":55512},{"block":false,"categoryid":317,"description":"An efficient theorem prover","ebuildids":[794143,839704],"firstseen":"2017-01-02T14:37:11.628924","name":"z3","packageid":66323,"summary":"Z3 is an efficient Satisfiability Modulo Theories (SMT) solver from Microsoft Research. Z3 is a solver for symbolic logic, a foundation for many software engineering tools. SMT solvers rely on a tight integration of specialized engines of proof. Each engine owns a piece of the global puzzle and implements specialized algorithms. For example, Z3’s engine for arithmetic integrates Simplex, cuts and polynomial reasoning, while an engine for strings are regular expressions integrate methods for symbolic derivatives of regular languages. A theme shared among many of the algorithms is how they exploit a duality between finding satisfying solutions and finding refutation proofs. The solver also integrates engines for global and local inferences and global propagation. Z3 is used in a wide range of software engineering applications, ranging from program verification, compiler validation, testing, fuzzing using dynamic symbolic execution, model-based software development, network verification, and optimization."}],"depending":[],"ebuilds":[{"archs":["~amd64","~x86"],"ebuildid":839704,"firstseen":"2024-09-30T19:44:40.351748","license":"BSD","moddate":"2025-05-06T18:09:01","packageid":73738,"repoid":1,"slot":"0\/4.9","uses":["debug","z3"],"version":"4.9"},{"archs":["~amd64","~x86"],"ebuildid":794143,"firstseen":"2023-07-15T01:50:27.786931","license":"BSD","moddate":"2025-05-06T18:09:01","packageid":73738,"repoid":1,"slot":"0\/4.8","uses":["debug","z3"],"version":"4.8"}],"masks":[],"package":{"categoryid":317,"description":"The Vampire Prover, theorem prover for first-order logic","firstseen":"2021-12-11T15:06:40.720898","name":"vampire","packageid":73738,"summary":"Vampire is a theorem prover, that is, a system able to prove theorems — although now it can do much more! Its main focus is in proving theorems in first-order logic but it can also prove non-theorems and build finite models, as well as reasoning in combinations of theories, such as arithmetic, arrays, and datatypes, and with higher-order logic. The development of Vampire began in 1994 and has survived a number of rewritings."},"rdependencies":[{"block":false,"categoryid":393,"description":"Library for arbitrary-precision arithmetic on different type of numbers","ebuildids":[794143,839704],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"toolchain@gentoo.org","maintainername":"Gentoo Toolchain Project","name":"gmp","packageid":55512},{"block":false,"categoryid":317,"description":"An efficient theorem prover","ebuildids":[794143,839704],"firstseen":"2017-01-02T14:37:11.628924","name":"z3","packageid":66323,"summary":"Z3 is an efficient Satisfiability Modulo Theories (SMT) solver from Microsoft Research. Z3 is a solver for symbolic logic, a foundation for many software engineering tools. SMT solvers rely on a tight integration of specialized engines of proof. Each engine owns a piece of the global puzzle and implements specialized algorithms. For example, Z3’s engine for arithmetic integrates Simplex, cuts and polynomial reasoning, while an engine for strings are regular expressions integrate methods for symbolic derivatives of regular languages. A theme shared among many of the algorithms is how they exploit a duality between finding satisfying solutions and finding refutation proofs. The solver also integrates engines for global and local inferences and global propagation. Z3 is used in a wide range of software engineering applications, ranging from program verification, compiler validation, testing, fuzzing using dynamic symbolic execution, model-based software development, network verification, and optimization."}],"repos":[{"branch":"master","lastcommit":"83b1268c5aac6ae9b0760d1fb99a3cf736f62f25","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/vprover\/vampire\/","https:\/\/vprover.github.io\/"],"uses":[{"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 support for sci-mathematics\/z3","isdefault":true,"packageid":73738,"use":"z3"}]}