{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":431250460,"defaultBranch":"main","name":"lean-smt","ownerLogin":"ufmg-smite","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-11-23T20:54:14.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/93679751?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1716820433.0","currentOid":""},"activityList":{"items":[{"before":"91ac7f46c83137327715874d27851b7421a40725","after":"b332ae49450b88c5ead40d66e4d786cb5d991ea9","ref":"refs/heads/main","pushedAt":"2024-07-12T05:48:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fix bug with Iff elimination. (#123)","shortMessageHtmlLink":"Fix bug with Iff elimination. (#123)"}},{"before":"2899f02744cc12636f71c04e200bce0b308f73b5","after":"91ac7f46c83137327715874d27851b7421a40725","ref":"refs/heads/main","pushedAt":"2024-07-08T00:23:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"chore: bump Lean to v4.9.0 (#119)\n\n* bump Lean to v4.9.0\r\n\r\n* Fix compilation of Smt.Real\r\n\r\n* Fix expected outputs of most test cases\r\n\r\n* import Real.Star instead of Real.Basic\r\n\r\n* Revert import Real.Star -> Real.Basic, update test case to reflect failure","shortMessageHtmlLink":"chore: bump Lean to v4.9.0 (#119)"}},{"before":"921d31e4d5f5167fc376cb65b38f51f98cbfc3fd","after":"2899f02744cc12636f71c04e200bce0b308f73b5","ref":"refs/heads/main","pushedAt":"2024-06-24T03:41:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Split proof reconstruction for integers and reals. (#112)","shortMessageHtmlLink":"Split proof reconstruction for integers and reals. (#112)"}},{"before":"139bf3da7ec9dfcf9a3278417a4b98e1bbe71ed0","after":"921d31e4d5f5167fc376cb65b38f51f98cbfc3fd","ref":"refs/heads/main","pushedAt":"2024-06-24T03:11:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fix solver tests. (#117)","shortMessageHtmlLink":"Fix solver tests. (#117)"}},{"before":"1c870041542025ee49184112b8ca372adb9b7ecd","after":"139bf3da7ec9dfcf9a3278417a4b98e1bbe71ed0","ref":"refs/heads/main","pushedAt":"2024-06-22T19:51:45.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Sync with cvc5 main. (#116)","shortMessageHtmlLink":"Sync with cvc5 main. (#116)"}},{"before":"9dff10149ddf5e8941c973ebedab1743920e6812","after":"1c870041542025ee49184112b8ca372adb9b7ecd","ref":"refs/heads/main","pushedAt":"2024-06-12T13:06:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Reprove theorems for proof rules and rewrites for integers. (#114)\n\n* Reprove theorems for proof rules and rewrites for integers.\r\n\r\n* Use newly available theorems.","shortMessageHtmlLink":"Reprove theorems for proof rules and rewrites for integers. (#114)"}},{"before":"64d482b74c32913120a7e6de9145e92433532200","after":"9dff10149ddf5e8941c973ebedab1743920e6812","ref":"refs/heads/main","pushedAt":"2024-06-12T11:20:11.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"chore: bump to v4.8.0 (#113)\n\n* bump to v4.8.0\r\n\r\n* chore: revert `lean-cvc5` dependency\r\n\r\n* chore: apply PR review\r\n\r\n* chore: ignore macos trash files\r\n\r\n* chore: homogeneous lakefile requires\r\n\r\n* chore: bump tests to 4.8\r\n\r\n* chore: cvc5 dependency\r\n\r\n* fix: bumping more files to 4.8\r\n\r\n* fix: use `rawNatLit?` not `nat?` on `Lean.expr`\r\n\r\n* chore: update test expected outputs\r\n\r\n* chore: gitignore","shortMessageHtmlLink":"chore: bump to v4.8.0 (#113)"}},{"before":"95747e9bf4bda4f80a7bf359cf774b8514633328","after":"64d482b74c32913120a7e6de9145e92433532200","ref":"refs/heads/main","pushedAt":"2024-06-07T18:52:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Support more arithmetic rewrites. (#111)","shortMessageHtmlLink":"Support more arithmetic rewrites. (#111)"}},{"before":"eb670925cd95ae23a9cd0826c570944f042ee0b9","after":"95747e9bf4bda4f80a7bf359cf774b8514633328","ref":"refs/heads/main","pushedAt":"2024-06-07T07:55:33.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fixes to reconstruction of resolution and other rules. (#110)","shortMessageHtmlLink":"Fixes to reconstruction of resolution and other rules. (#110)"}},{"before":"fb6743ae6bb3bd1a55b1776b8cb326bfd8bbc87a","after":"eb670925cd95ae23a9cd0826c570944f042ee0b9","ref":"refs/heads/main","pushedAt":"2024-06-07T00:43:04.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"orN-resolution proof (#109)\n\n* orN-proof\r\n\r\n* re-adjustment\r\n\r\n* small change\r\n\r\n* fixed","shortMessageHtmlLink":"orN-resolution proof (#109)"}},{"before":"6c40c29c5aef20f36ae69bc2af15eb536b1a7d4e","after":"fb6743ae6bb3bd1a55b1776b8cb326bfd8bbc87a","ref":"refs/heads/main","pushedAt":"2024-06-06T19:55:50.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Add support for QUANT_MINISCOPE rewrite rule. (#108)","shortMessageHtmlLink":"Add support for QUANT_MINISCOPE rewrite rule. (#108)"}},{"before":"9dbfde40c19776fe64b4b3ba1554033a8d7382de","after":"6c40c29c5aef20f36ae69bc2af15eb536b1a7d4e","ref":"refs/heads/main","pushedAt":"2024-06-02T14:41:41.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Sync with cvc5 main. (#107)","shortMessageHtmlLink":"Sync with cvc5 main. (#107)"}},{"before":"af0c495e022407d14186cca614018cb3cdddb0c5","after":null,"ref":"refs/heads/abdoo8080-patch-1","pushedAt":"2024-05-27T14:33:53.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"}},{"before":"3049bb11f9fcc0ac3a2fec646da805158bf9d887","after":"9dbfde40c19776fe64b4b3ba1554033a8d7382de","ref":"refs/heads/main","pushedAt":"2024-05-27T14:33:47.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Update README.md (#106)\n\n* Update README.md\r\n\r\n* Update README.md","shortMessageHtmlLink":"Update README.md (#106)"}},{"before":"72751828b15b5d6c4567a03c6afd2ea28159ebc9","after":"af0c495e022407d14186cca614018cb3cdddb0c5","ref":"refs/heads/abdoo8080-patch-1","pushedAt":"2024-05-27T14:33:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Update README.md","shortMessageHtmlLink":"Update README.md"}},{"before":null,"after":"72751828b15b5d6c4567a03c6afd2ea28159ebc9","ref":"refs/heads/abdoo8080-patch-1","pushedAt":"2024-05-27T14:32:22.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Update README.md","shortMessageHtmlLink":"Update README.md"}},{"before":"46c5a9eec31a4b4209be1af7c6c5a845cfd6ae0f","after":"3049bb11f9fcc0ac3a2fec646da805158bf9d887","ref":"refs/heads/main","pushedAt":"2024-05-27T11:41:41.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Support MacOS AArch64. (#105)","shortMessageHtmlLink":"Support MacOS AArch64. (#105)"}},{"before":"b720017c218ce9d726d397f3c68654768cfe88cb","after":"46c5a9eec31a4b4209be1af7c6c5a845cfd6ae0f","ref":"refs/heads/main","pushedAt":"2024-05-27T10:10:38.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fix bugs and support more Bool and quantifier rewrites. (#104)\n\n* Fix bugs and support more Bool and quantifier rewrites.\r\n\r\n* Switch to libstd++.","shortMessageHtmlLink":"Fix bugs and support more Bool and quantifier rewrites. (#104)"}},{"before":"73e3fdfa6fce81bb6010aa64c51a124ab963664d","after":"b720017c218ce9d726d397f3c68654768cfe88cb","ref":"refs/heads/main","pushedAt":"2024-05-25T08:02:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Only track fvars needed by translation. (#102)","shortMessageHtmlLink":"Only track fvars needed by translation. (#102)"}},{"before":"40caffdc4a7852d3e8df57bba38c6d257f9e7d6c","after":"73e3fdfa6fce81bb6010aa64c51a124ab963664d","ref":"refs/heads/main","pushedAt":"2024-05-23T06:59:09.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Split smt tactic into a meta program and a tactic driver. (#101)","shortMessageHtmlLink":"Split smt tactic into a meta program and a tactic driver. (#101)"}},{"before":"b28f919efb806ecd9994ac21ac43fa2fbdaea1a7","after":"40caffdc4a7852d3e8df57bba38c6d257f9e7d6c","ref":"refs/heads/main","pushedAt":"2024-05-23T03:47:55.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fix and optimize reconstruction of proofs with quantifiers. (#99)\n\n* Fix and optimize reconstruction of proofs with quantifiers.\r\n\r\n* Update error message.","shortMessageHtmlLink":"Fix and optimize reconstruction of proofs with quantifiers. (#99)"}},{"before":"8e32551d2b06470ae6b1f27089cba580f2388508","after":"b28f919efb806ecd9994ac21ac43fa2fbdaea1a7","ref":"refs/heads/main","pushedAt":"2024-05-23T02:48:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fix and optimize AC norm. (#98)\n\n* Fix and optimize AC norm.\r\n\r\n* Fix error message.","shortMessageHtmlLink":"Fix and optimize AC norm. (#98)"}},{"before":"04048378dabbb0c42862495f4e8e8574be57379e","after":"8e32551d2b06470ae6b1f27089cba580f2388508","ref":"refs/heads/main","pushedAt":"2024-05-14T08:42:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fix and optimize resolution code. (#95)","shortMessageHtmlLink":"Fix and optimize resolution code. (#95)"}},{"before":"fc8b5f9157743800b875ad687ca10cdc5c90dd3a","after":"04048378dabbb0c42862495f4e8e8574be57379e","ref":"refs/heads/main","pushedAt":"2024-05-09T00:36:04.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Support bitblasted addition. (#93)","shortMessageHtmlLink":"Support bitblasted addition. (#93)"}},{"before":"3e7268f4e95b9ad1aa4bc2bfcaa0ee484415a72c","after":"fc8b5f9157743800b875ad687ca10cdc5c90dd3a","ref":"refs/heads/main","pushedAt":"2024-05-09T00:06:33.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Cleanup tracing and profiling options. (#92)","shortMessageHtmlLink":"Cleanup tracing and profiling options. (#92)"}},{"before":"0703bebd02a5f3bf8ad3b3f0167b8ef85ed2d6cd","after":null,"ref":"refs/heads/license","pushedAt":"2024-05-07T06:19:53.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"}},{"before":"65720b942f50a356e60fe1832bb1fe8bcdb20ddd","after":"3e7268f4e95b9ad1aa4bc2bfcaa0ee484415a72c","ref":"refs/heads/main","pushedAt":"2024-05-06T22:25:26.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Support reconstruction of more BV terms. (#91)","shortMessageHtmlLink":"Support reconstruction of more BV terms. (#91)"}},{"before":"f5a2b42fe3272ba714f595d2a15e83ea03ca17f7","after":"65720b942f50a356e60fe1832bb1fe8bcdb20ddd","ref":"refs/heads/main","pushedAt":"2024-05-06T22:08:51.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Fix and optimize smtCongr tactic. (#90)","shortMessageHtmlLink":"Fix and optimize smtCongr tactic. (#90)"}},{"before":"c066cc15c17d463ee226960b0c4eb0e2125fdf3a","after":"f5a2b42fe3272ba714f595d2a15e83ea03ca17f7","ref":"refs/heads/main","pushedAt":"2024-05-06T07:48:04.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Support EXISTS_ELIM and DISTINCT_ELIM rules. (#89)\n\n* Support EXISTS_ELIM and DISTINCT_ELIM rules.\r\n\r\n* Simplify distinct definition.","shortMessageHtmlLink":"Support EXISTS_ELIM and DISTINCT_ELIM rules. (#89)"}},{"before":"52770084ab23f9778734ea008c8e9d266791ad56","after":"c066cc15c17d463ee226960b0c4eb0e2125fdf3a","ref":"refs/heads/main","pushedAt":"2024-04-29T23:11:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"abdoo8080","name":"Abdalrhman Mohamed","path":"/abdoo8080","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/32971963?s=80&v=4"},"commit":{"message":"Update LICENSE (#88)","shortMessageHtmlLink":"Update LICENSE (#88)"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEfYPGrQA","startCursor":null,"endCursor":null}},"title":"Activity ยท ufmg-smite/lean-smt"}