{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":95927890,"defaultBranch":"master","name":"crab","ownerLogin":"seahorn","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2017-06-30T22:21:48.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/11098044?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1712694061.0","currentOid":""},"activityList":{"items":[{"before":"d2cabf90f754bc8964eae3bcf84ad1608eac8aad","after":"4d934fedac3a1ce123502d2afec8c9ee86c5a89b","ref":"refs/heads/dev","pushedAt":"2024-04-23T14:13:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(flat-bool): to_linear_constraints_system","shortMessageHtmlLink":"fix(flat-bool): to_linear_constraints_system"}},{"before":"352dc1dbff5510447bf2e81fc0c8d724603905c4","after":"d2cabf90f754bc8964eae3bcf84ad1608eac8aad","ref":"refs/heads/dev","pushedAt":"2024-04-12T20:28:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix: compiler error if bignum used as weights in split_oct","shortMessageHtmlLink":"fix: compiler error if bignum used as weights in split_oct"}},{"before":"733d448f3a3e676f4f1b807baaf0ccc487e772f7","after":null,"ref":"refs/heads/pplite-native","pushedAt":"2024-04-09T20:21:01.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"}},{"before":"733d448f3a3e676f4f1b807baaf0ccc487e772f7","after":"352dc1dbff5510447bf2e81fc0c8d724603905c4","ref":"refs/heads/dev","pushedAt":"2024-04-09T18:43:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"ci: run pplite","shortMessageHtmlLink":"ci: run pplite"}},{"before":"d257cfcd801f4091fd9c6cb6fa38549ce9fdbee9","after":"733d448f3a3e676f4f1b807baaf0ccc487e772f7","ref":"refs/heads/dev","pushedAt":"2024-04-09T18:40:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat: native interface for PPLite\n\nEnable using option -DCRAB_USE_PPLITE_NATIVE=ON\n\nfix(test): HAVE_PPLITE does not imply HAVE_APRON\n\nBefore having a native interface for pplite, the pragma HAVE_PPLITE\nimplied HAVE_APRON because pplite was necessarily using the apron\ninterface. However after, that implication does not necessarily\nholds. However the decoupled domain (specifically convert_to) expects\nboth HAVE_APRON and HAVE_PPLITE enabled if template parameter is\ninstantiated with apron_asc_dsc_pair.","shortMessageHtmlLink":"feat: native interface for PPLite"}},{"before":"27bdf7c4ad6c75ed0792915444af85fc565ed29a","after":"733d448f3a3e676f4f1b807baaf0ccc487e772f7","ref":"refs/heads/pplite-native","pushedAt":"2024-04-09T18:38:25.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat: native interface for PPLite\n\nEnable using option -DCRAB_USE_PPLITE_NATIVE=ON\n\nfix(test): HAVE_PPLITE does not imply HAVE_APRON\n\nBefore having a native interface for pplite, the pragma HAVE_PPLITE\nimplied HAVE_APRON because pplite was necessarily using the apron\ninterface. However after, that implication does not necessarily\nholds. However the decoupled domain (specifically convert_to) expects\nboth HAVE_APRON and HAVE_PPLITE enabled if template parameter is\ninstantiated with apron_asc_dsc_pair.","shortMessageHtmlLink":"feat: native interface for PPLite"}},{"before":"49386eb0e477f8ee33e2e702341d90ce011494dc","after":"27bdf7c4ad6c75ed0792915444af85fc565ed29a","ref":"refs/heads/pplite-native","pushedAt":"2024-04-09T01:11:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"test: expected results for pplite native","shortMessageHtmlLink":"test: expected results for pplite native"}},{"before":"abcb8ed08b6e8bacc8655013c29b6ac570ba8d88","after":"49386eb0e477f8ee33e2e702341d90ce011494dc","ref":"refs/heads/pplite-native","pushedAt":"2024-04-09T01:08:28.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"docker: pplite native","shortMessageHtmlLink":"docker: pplite native"}},{"before":"315758770e1cecf66269ac5939dd160e1f00a62d","after":"d257cfcd801f4091fd9c6cb6fa38549ce9fdbee9","ref":"refs/heads/dev","pushedAt":"2024-04-08T18:14:28.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"test: expected_results.elina.out","shortMessageHtmlLink":"test: expected_results.elina.out"}},{"before":"8e6fb0b5da6895104feeeaf3a7b27285bea79620","after":"315758770e1cecf66269ac5939dd160e1f00a62d","ref":"refs/heads/dev","pushedAt":"2024-04-01T21:32:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(flat-bool-domain): sext\n\nThe analysis of sext was wrong in the flat boolean domain.\nThe bug was introduced by commit 106878f.\nThis commit tried to remove any domain-specific reasoning.","shortMessageHtmlLink":"fix(flat-bool-domain): sext"}},{"before":"027b5ff0f16c81d2296eba412b855757e54e0a71","after":"abcb8ed08b6e8bacc8655013c29b6ac570ba8d88","ref":"refs/heads/pplite-native","pushedAt":"2024-02-06T04:57:58.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(test): HAVE_PPLITE does not imply HAVE_APRON\n\nBefore having a native interface for pplite, the pragma HAVE_PPLITE\nimplied HAVE_APRON because pplite was necessarily using the apron\ninterface. However after, that implication does not necessarily\nholds. However the decoupled domain (specifically convert_to) expects\nboth HAVE_APRON and HAVE_PPLITE enabled if template parameter is\ninstantiated with apron_asc_dsc_pair.","shortMessageHtmlLink":"fix(test): HAVE_PPLITE does not imply HAVE_APRON"}},{"before":null,"after":"027b5ff0f16c81d2296eba412b855757e54e0a71","ref":"refs/heads/pplite-native","pushedAt":"2023-12-03T04:07:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat: native interface for PPLite\n\nEnable using option -DCRAB_USE_PPLITE_NATIVE=ON","shortMessageHtmlLink":"feat: native interface for PPLite"}},{"before":"300f7118f269e2b9188e936564370fb5d573efb4","after":"8e6fb0b5da6895104feeeaf3a7b27285bea79620","ref":"refs/heads/dev","pushedAt":"2023-09-21T23:28:15.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"chore: remove compiler warning unary_function deprecated","shortMessageHtmlLink":"chore: remove compiler warning unary_function deprecated"}},{"before":"0c2fb25c830d88aeef025461ed120c922c4937c7","after":"300f7118f269e2b9188e936564370fb5d573efb4","ref":"refs/heads/dev","pushedAt":"2023-09-21T03:05:58.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(test): instantiate only if APRON/PPLITE enabled","shortMessageHtmlLink":"fix(test): instantiate only if APRON/PPLITE enabled"}},{"before":"26dacabe6c8d3b65d278c92271a0ab24f3eda153","after":"146f5399c72ff508f176e6392e490647ac657ce7","ref":"refs/heads/master","pushedAt":"2023-09-21T02:58:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(ci): run ci on dev branch","shortMessageHtmlLink":"fix(ci): run ci on dev branch"}},{"before":"f24db976e7bd67c86d0dd2a158e5b26b1b883dab","after":"0c2fb25c830d88aeef025461ed120c922c4937c7","ref":"refs/heads/dev","pushedAt":"2023-09-20T13:55:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(test): instantiate only if APRON/PPLITE enabled","shortMessageHtmlLink":"fix(test): instantiate only if APRON/PPLITE enabled"}},{"before":"838d8468dd252be3c5114a8730fd78dcf3d63671","after":"f24db976e7bd67c86d0dd2a158e5b26b1b883dab","ref":"refs/heads/dev","pushedAt":"2023-09-18T15:51:46.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"tests: adapt expected format","shortMessageHtmlLink":"tests: adapt expected format"}},{"before":"30682068cc64d0a9013aa8d1f74572c962ff7d74","after":"26dacabe6c8d3b65d278c92271a0ab24f3eda153","ref":"refs/heads/master","pushedAt":"2023-09-16T22:15:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"docker: fix dockerfiles","shortMessageHtmlLink":"docker: fix dockerfiles"}},{"before":"a288b5e37e016c4b1c116484716425aef5b6da2b","after":"30682068cc64d0a9013aa8d1f74572c962ff7d74","ref":"refs/heads/master","pushedAt":"2023-09-16T20:48:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"ci: fix yaml syntax","shortMessageHtmlLink":"ci: fix yaml syntax"}},{"before":"e43a7a1c4db0af8dfcfe8d087b7f9f0f0a6d0df3","after":"a288b5e37e016c4b1c116484716425aef5b6da2b","ref":"refs/heads/master","pushedAt":"2023-09-16T20:44:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"ci: split into more actions","shortMessageHtmlLink":"ci: split into more actions"}},{"before":"b63cb256a09888416c3209ff6d678a204813e5c2","after":"838d8468dd252be3c5114a8730fd78dcf3d63671","ref":"refs/heads/dev","pushedAt":"2023-09-16T15:44:09.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"tests: adapt expected format","shortMessageHtmlLink":"tests: adapt expected format"}},{"before":"e401a1eb8292be5589930d8968e654bbfbbf7f49","after":"e43a7a1c4db0af8dfcfe8d087b7f9f0f0a6d0df3","ref":"refs/heads/master","pushedAt":"2023-09-15T17:02:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(bool-domain): propagation in assume(not b)\n\nThe kind of facts that we keep track in m_bool_to_lincsts (resp\nm_bool_to_bools) is of the form:\n\n if b becomes true then constraint C (resp. boolean b') MUST be true\n\nThus, if b is false then nothing can really be said about C (resp b')\nbut we were propagating incorrectly that C (resp b') was false.\n\nWe added a test that passed incorrectly before (assertion was proven)\nand now it doesn't pass anymore (assertion cannot be proven).","shortMessageHtmlLink":"fix(bool-domain): propagation in assume(not b)"}},{"before":"02880544846a8bba61f4c1baa22c5681765060c1","after":"b63cb256a09888416c3209ff6d678a204813e5c2","ref":"refs/heads/dev","pushedAt":"2023-07-28T21:09:33.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(wto): add const&","shortMessageHtmlLink":"fix(wto): add const&"}},{"before":"70cc59952c8d0fb6e5baea71da43354da408ab16","after":"e401a1eb8292be5589930d8968e654bbfbbf7f49","ref":"refs/heads/master","pushedAt":"2023-07-23T21:19:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"feat(cfg): return mutable reference to statement","shortMessageHtmlLink":"feat(cfg): return mutable reference to statement"}},{"before":"4b05236381796c5d3cfafd790f222ce0922de135","after":"02880544846a8bba61f4c1baa22c5681765060c1","ref":"refs/heads/dev","pushedAt":"2023-07-15T19:51:18.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(wto): add const&","shortMessageHtmlLink":"fix(wto): add const&"}},{"before":"72d8c5220b9b50eeba27c42f97b4c92d3dcc1834","after":"70cc59952c8d0fb6e5baea71da43354da408ab16","ref":"refs/heads/master","pushedAt":"2023-07-14T07:36:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"ci: run in Release mode avoiding run out of disk","shortMessageHtmlLink":"ci: run in Release mode avoiding run out of disk"}},{"before":"bbe2f9ecc79b19d8320a05a507f203884239997c","after":"4b05236381796c5d3cfafd790f222ce0922de135","ref":"refs/heads/dev","pushedAt":"2023-07-09T19:57:14.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(apron_domain): adapt to new pplite 0.11 api\n\nThis fix is related to commit f04d015cd0dab117b9560afa1bb3be70ebecf8d9","shortMessageHtmlLink":"fix(apron_domain): adapt to new pplite 0.11 api"}},{"before":"1c737592f972ab771c516b438bd18a6c4aa75f36","after":"72d8c5220b9b50eeba27c42f97b4c92d3dcc1834","ref":"refs/heads/master","pushedAt":"2023-07-09T19:52:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"reverted commit\n\nThis commit reverts 19407e71199e3120d7d98da2eff2fc284dbe83c4","shortMessageHtmlLink":"reverted commit"}},{"before":"10611e830c38f752cff54cc26f0fc01c07337f76","after":"bbe2f9ecc79b19d8320a05a507f203884239997c","ref":"refs/heads/dev","pushedAt":"2023-07-07T20:47:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"fix(apron_domain): adapt to new pplite 0.11 api\n\nThis fix is related to commit f04d015cd0dab117b9560afa1bb3be70ebecf8d9","shortMessageHtmlLink":"fix(apron_domain): adapt to new pplite 0.11 api"}},{"before":"67c1d352283128bbabc4616b2624bf370948ee04","after":"1c737592f972ab771c516b438bd18a6c4aa75f36","ref":"refs/heads/master","pushedAt":"2023-07-07T20:45:48.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"caballa","name":"Jorge Navas","path":"/caballa","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5025780?s=80&v=4"},"commit":{"message":"refactor(value-part-domain): improve precision with disequalities","shortMessageHtmlLink":"refactor(value-part-domain): improve precision with disequalities"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEOCfYLgA","startCursor":null,"endCursor":null}},"title":"Activity ยท seahorn/crab"}