{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":42260199,"defaultBranch":"dev","name":"ultimate","ownerLogin":"ultimate-pa","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-09-10T17:37:47.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/13460489?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726762823.0","currentOid":""},"activityList":{"items":[{"before":"99cac5aa2b47b672026786322ebe1b32bfb9662a","after":"50cff0d427da50cf1966c8e44900bc0c05c99662","ref":"refs/heads/dev","pushedAt":"2024-09-20T16:13:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Add some further simplifications for backtranslation","shortMessageHtmlLink":"Add some further simplifications for backtranslation"}},{"before":"1110f613a3f26b72d8fa1b38da398ec5d8d04ea9","after":"99cac5aa2b47b672026786322ebe1b32bfb9662a","ref":"refs/heads/dev","pushedAt":"2024-09-20T15:57:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Add missing cases","shortMessageHtmlLink":"Add missing cases"}},{"before":"25c32e0fee9db7cdc642f97d4e386843fdae3b06","after":"1110f613a3f26b72d8fa1b38da398ec5d8d04ea9","ref":"refs/heads/dev","pushedAt":"2024-09-20T15:36:09.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Check >= and <= on ranges to allow more simplification","shortMessageHtmlLink":"Check &gt;= and &lt;= on ranges to allow more simplification"}},{"before":"1864bafbc1b595682c8f71718fd620c42f370a4c","after":"25c32e0fee9db7cdc642f97d4e386843fdae3b06","ref":"refs/heads/dev","pushedAt":"2024-09-20T15:16:06.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Report backtranslation issues for unsupported operators","shortMessageHtmlLink":"Report backtranslation issues for unsupported operators"}},{"before":"1e8eb79e3b8b91e0c670b5f39ca27f40b0846ff1","after":"a3200d1d3584b720ed963d32cc1bfbb100be2bdd","ref":"refs/heads/wip/fs/yaml-violation-witnesses","pushedAt":"2024-09-20T13:31:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HelenAnnaMeyer","name":"Helen Meyer","path":"/HelenAnnaMeyer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148922823?s=80&v=4"},"commit":{"message":"check if last waypoint is target","shortMessageHtmlLink":"check if last waypoint is target"}},{"before":"16db84067fa4d4b1675a8004bdb575206b0a6ff6","after":"1864bafbc1b595682c8f71718fd620c42f370a4c","ref":"refs/heads/dev","pushedAt":"2024-09-20T09:48:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Optimize backtranslation for division","shortMessageHtmlLink":"Optimize backtranslation for division"}},{"before":"1ea3e5331eaac9a86847aee0a682124e3006de97","after":"16db84067fa4d4b1675a8004bdb575206b0a6ff6","ref":"refs/heads/dev","pushedAt":"2024-09-20T09:27:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Revert eed97c8\nThe arithmetical operations on Boogie have the semantics over mathematical integers.\nTherefore we want to avoid wraparrounds for that case, when backtranslating invariants to C.\nThis happens by adding casts during backtranslation based on simple range calculations.\nFor example, given the expression x * 2 in Boogie (where x is an variable of type unsigned in the C program),\nwe should add a cast to (unsigned) long long to keep the semantics of that expression during backtranslation.","shortMessageHtmlLink":"Revert <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/ultimate-pa/ultimate/commit/eed97c8ba83de894d560df8d51a16b943be74a4e/hovercard\" href=\"https://github.com/ultimate-pa/ultimate/commit/eed97c8ba83de894d560df8d51a16b943be74a4e\"><tt>eed97c8</tt></a>"}},{"before":null,"after":"274e47332c146424445e980fb95e85b6f667127b","ref":"refs/heads/dependabot/bundler/trunk/source/WebsiteStatic/google-protobuf-4.27.5","pushedAt":"2024-09-19T16:20:23.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"},"commit":{"message":"Bump google-protobuf in /trunk/source/WebsiteStatic\n\nBumps [google-protobuf](https://github.com/protocolbuffers/protobuf) from 4.27.3 to 4.27.5.\n- [Release notes](https://github.com/protocolbuffers/protobuf/releases)\n- [Changelog](https://github.com/protocolbuffers/protobuf/blob/main/protobuf_release.bzl)\n- [Commits](https://github.com/protocolbuffers/protobuf/commits)\n\n---\nupdated-dependencies:\n- dependency-name: google-protobuf\n  dependency-type: indirect\n...\n\nSigned-off-by: dependabot[bot] <support@github.com>","shortMessageHtmlLink":"Bump google-protobuf in /trunk/source/WebsiteStatic"}},{"before":"1117dc532994bdc05d4a3c8a8a3db2cc30046587","after":"30f502301c75574350c043689a8c96d334d09962","ref":"refs/heads/wip/dk/conditional-comm","pushedAt":"2024-09-19T12:49:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ebbima","name":null,"path":"/ebbima","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66482162?s=80&v=4"},"commit":{"message":"Update PartialOrderCegarLoop.java","shortMessageHtmlLink":"Update PartialOrderCegarLoop.java"}},{"before":"48dbcd425b8f6aa80a1acb9f818e1b4359449713","after":"1117dc532994bdc05d4a3c8a8a3db2cc30046587","ref":"refs/heads/wip/dk/conditional-comm","pushedAt":"2024-09-19T12:27:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ebbima","name":null,"path":"/ebbima","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66482162?s=80&v=4"},"commit":{"message":"tiny fix and added a writer for debugging","shortMessageHtmlLink":"tiny fix and added a writer for debugging"}},{"before":null,"after":"b37cf8866c2595d4216df86cf81d26532a94b7d7","ref":"refs/heads/wip/fs/test-fixes","pushedAt":"2024-09-19T11:17:10.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Move failing automata tests to openBugs (#611)","shortMessageHtmlLink":"Move failing automata tests to openBugs (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1527454582\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ultimate-pa/ultimate/issues/611\" data-hovercard-type=\"issue\" data-hovercard-url=\"/ultimate-pa/ultimate/issues/611/hovercard\" href=\"https://github.com/ultimate-pa/ultimate/issues/611\">#611</a>)"}},{"before":"63aa41e68dca1377da88366d3db2fdc1089628e4","after":"1ea3e5331eaac9a86847aee0a682124e3006de97","ref":"refs/heads/dev","pushedAt":"2024-09-19T08:22:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"},"commit":{"message":"add range calculation for euclidean modulo","shortMessageHtmlLink":"add range calculation for euclidean modulo"}},{"before":"6998d33abc19b5d7a098a1046b4b8253b4ab1a9e","after":"8a4f03cdb1f0911b7ab5c3dc45904e470d598cc6","ref":"refs/heads/TestGeneration","pushedAt":"2024-09-18T22:42:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MaxBarth95","name":"Max barth","path":"/MaxBarth95","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9918718?s=80&v=4"},"commit":{"message":"fix forgott to pop() and provide no programExecution in case of reuse","shortMessageHtmlLink":"fix forgott to pop() and provide no programExecution in case of reuse"}},{"before":"581c3b56179bbeedbda0a66d9c72498f2ddcf2c1","after":"6998d33abc19b5d7a098a1046b4b8253b4ab1a9e","ref":"refs/heads/TestGeneration","pushedAt":"2024-09-18T22:20:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MaxBarth95","name":"Max barth","path":"/MaxBarth95","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9918718?s=80&v=4"},"commit":{"message":"Reveted using cfg script for reuse, overhead too big","shortMessageHtmlLink":"Reveted using cfg script for reuse, overhead too big"}},{"before":"196b9cdc9293e3ed8b120fcb8fe9411c65235c03","after":"48dbcd425b8f6aa80a1acb9f818e1b4359449713","ref":"refs/heads/wip/dk/conditional-comm","pushedAt":"2024-09-18T14:25:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ebbima","name":null,"path":"/ebbima","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66482162?s=80&v=4"},"commit":{"message":"Counterexample approach\n\nA first version of the \"counterexample approach\" implemented as a special case of the IA-Approach","shortMessageHtmlLink":"Counterexample approach"}},{"before":"ca387f627c9d61c541efe82dc49406bf51e53651","after":"1e8eb79e3b8b91e0c670b5f39ca27f40b0846ff1","ref":"refs/heads/wip/fs/yaml-violation-witnesses","pushedAt":"2024-09-18T12:22:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HelenAnnaMeyer","name":"Helen Meyer","path":"/HelenAnnaMeyer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148922823?s=80&v=4"},"commit":{"message":"integrated unneccessary helper functions","shortMessageHtmlLink":"integrated unneccessary helper functions"}},{"before":"c2cce925e105440734b066ce70b5b7423d36ab24","after":"63aa41e68dca1377da88366d3db2fdc1089628e4","ref":"refs/heads/dev","pushedAt":"2024-09-18T10:39:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Write correct data-model to YAML witness","shortMessageHtmlLink":"Write correct data-model to YAML witness"}},{"before":"d4b8d210e8a14f86561d9edc4d2deecf562463f0","after":"c2cce925e105440734b066ce70b5b7423d36ab24","ref":"refs/heads/dev","pushedAt":"2024-09-18T09:13:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Suppress backtranslation warnings for program states","shortMessageHtmlLink":"Suppress backtranslation warnings for program states"}},{"before":"ec70827bc5a9499de3ab433542fb790120f6023f","after":null,"ref":"refs/heads/wip/dk/fhvalidity-fix","pushedAt":"2024-09-18T09:12:22.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"}},{"before":"01ef5de87e82227ad4dfaf1b677f6254f05e78e0","after":"d4b8d210e8a14f86561d9edc4d2deecf562463f0","ref":"refs/heads/dev","pushedAt":"2024-09-18T09:12:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"},"commit":{"message":"Fix Floyd/Hoare validity check for Icfgs: actually check something\n\nPreviously, the check did not actually check anything, because the\nsuccessor edges were calculated incorrectly and, in particular for\ninitial states, were always empty.\n\nWe also need to filter summary edges for implemented procedures as\nthey are not expected to be inductive. This was previously done in\nHoareAnnotationChecker [1] previous to PR #671.\n\n[1] https://github.com/ultimate-pa/ultimate/blob/19fd058c3d438585a4f478206c978f85e13399ca/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/predicates/HoareAnnotationChecker.java#L141-L143","shortMessageHtmlLink":"Fix Floyd/Hoare validity check for Icfgs: actually check something"}},{"before":"5bcff13741759dbf42c2064c0f1b45d43b27b317","after":"01ef5de87e82227ad4dfaf1b677f6254f05e78e0","ref":"refs/heads/dev","pushedAt":"2024-09-17T22:26:14.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"},"commit":{"message":"fix range calculation for euclidean division","shortMessageHtmlLink":"fix range calculation for euclidean division"}},{"before":"8db44d33b630cb2e30071bdcaf3cda09af80307f","after":"581c3b56179bbeedbda0a66d9c72498f2ddcf2c1","ref":"refs/heads/TestGeneration","pushedAt":"2024-09-17T18:35:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MaxBarth95","name":"Max barth","path":"/MaxBarth95","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9918718?s=80&v=4"},"commit":{"message":"assert to cfg script even if no reuse","shortMessageHtmlLink":"assert to cfg script even if no reuse"}},{"before":"5ceec2340d127c4038c264986235ad2f36ecdeec","after":"ec70827bc5a9499de3ab433542fb790120f6023f","ref":"refs/heads/wip/dk/fhvalidity-fix","pushedAt":"2024-09-17T14:15:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"},"commit":{"message":"IcfgFloydHoareValidityCheck: fix getReturnSuccessors()","shortMessageHtmlLink":"IcfgFloydHoareValidityCheck: fix getReturnSuccessors()"}},{"before":"45f899e4361288adace4895f00fdba52bf1b8f4f","after":"5bcff13741759dbf42c2064c0f1b45d43b27b317","ref":"refs/heads/dev","pushedAt":"2024-09-17T14:13:27.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Fix range for not in backtranslation","shortMessageHtmlLink":"Fix range for not in backtranslation"}},{"before":"936ba784ada9bdd7f27d7df1c4a03369eebb2024","after":null,"ref":"refs/heads/wip/dk/typerange-fix","pushedAt":"2024-09-17T13:49:08.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"}},{"before":"3e443b1acbb89f2f930df48ef26113d83e4d3013","after":"45f899e4361288adace4895f00fdba52bf1b8f4f","ref":"refs/heads/dev","pushedAt":"2024-09-17T13:48:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"},"commit":{"message":"fix and refactor range calculation in Boogie2ACSL\n\n- Simplify the code by introducing class BigInterval\n  and using BigInterval for expression ranges in Boogie2ACSL.\n- Fix incorrect application of unsigned wraparound in\n  range calculation: euclidean modulo in interval is\n  not computed by applying euclidean modulo on bounds.\n\nThis should fix certain incorrect invariants currently produced.","shortMessageHtmlLink":"fix and refactor range calculation in Boogie2ACSL"}},{"before":"32cf4d90783c4dc26d24e5e3813c14241bf0ea36","after":"3e443b1acbb89f2f930df48ef26113d83e4d3013","ref":"refs/heads/dev","pushedAt":"2024-09-17T13:40:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Handle overapproximation flags in referee","shortMessageHtmlLink":"Handle overapproximation flags in referee"}},{"before":"420b7d8a2a4a4c015db54e353257673c55750a05","after":"936ba784ada9bdd7f27d7df1c4a03369eebb2024","ref":"refs/heads/wip/dk/typerange-fix","pushedAt":"2024-09-17T12:28:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"schuessf","name":"Frank Schüssele","path":"/schuessf","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3885674?s=80&v=4"},"commit":{"message":"Fix range for !","shortMessageHtmlLink":"Fix range for !"}},{"before":"fb77554f64a6298e9bc4605db360bdf11621b9c0","after":"5ceec2340d127c4038c264986235ad2f36ecdeec","ref":"refs/heads/wip/dk/fhvalidity-fix","pushedAt":"2024-09-16T19:10:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"},"commit":{"message":"fix Floyd-Hoare validity check for Icfgs: ignore summaries of implemented procedures\n\nThis was previously done in HoareAnnotationChecker [1], the predecessor of\nIcfgFloydHoareValidityCheck previous to PR #671. The filter was missed in\nthe PR, and not discovered so far because of another bug in IcfgFloydHoareValidityCheck\n(see fb77554f64).\n\n[1] https://github.com/ultimate-pa/ultimate/blob/19fd058c3d438585a4f478206c978f85e13399ca/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/predicates/HoareAnnotationChecker.java#L141-L143","shortMessageHtmlLink":"fix Floyd-Hoare validity check for Icfgs: ignore summaries of impleme…"}},{"before":"a126be574abf7a8a5a58ede8750dc68f51c08552","after":"420b7d8a2a4a4c015db54e353257673c55750a05","ref":"refs/heads/wip/dk/typerange-fix","pushedAt":"2024-09-16T18:21:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"maul-esel","name":"maul.esel","path":"/maul-esel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/800556?s=80&v=4"},"commit":{"message":"fix length calculation","shortMessageHtmlLink":"fix length calculation"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yMFQxNjoxMzowOC4wMDAwMDBazwAAAAS8KErN","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yMFQxNjoxMzowOC4wMDAwMDBazwAAAAS8KErN","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xNlQxODoyMTowMS4wMDAwMDBazwAAAAS3wDSF"}},"title":"Activity · ultimate-pa/ultimate"}