{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":14522461,"defaultBranch":"master","name":"smtinterpol","ownerLogin":"ultimate-pa","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2013-11-19T11:26:30.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/13460489?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1719158574.0","currentOid":""},"activityList":{"items":[{"before":"f8335c26707920b6afc26a9038f29674bd8c5003","after":"4bbdaf91a2209617989b351a873a2524fbaba21c","ref":"refs/heads/feature-ConstantTermNormalizer","pushedAt":"2024-06-23T17:51:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Heizmann","name":"Matthias Heizmann","path":"/Heizmann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1221834?s=80&v=4"},"commit":{"message":"Reduce number of params","shortMessageHtmlLink":"Reduce number of params"}},{"before":"98f115aa061342b7ff2b76b091f76de47f8335f6","after":"cca67e02084bb81bad7a0545098fb0a0a251dba2","ref":"refs/heads/master","pushedAt":"2024-06-23T17:40:08.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Merge pull request #149 from ultimate-pa/feature-all-smtcomp-logics\n\nAdd QF_UFBVFP and QF_UFNIRA","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2368624374\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ultimate-pa/smtinterpol/issues/149\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ultimate-pa/smtinterpol/pull/149/hovercard\" href=\"https://github.com/ultimate-pa/smtinterpol/pull/149\">#149</a> from ultimate-pa/feature-all-smtcomp-logics"}},{"before":null,"after":"f8335c26707920b6afc26a9038f29674bd8c5003","ref":"refs/heads/feature-ConstantTermNormalizer","pushedAt":"2024-06-23T16:02:54.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Heizmann","name":"Matthias Heizmann","path":"/Heizmann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1221834?s=80&v=4"},"commit":{"message":"Move ConstantTermNormalizer\n\n* Move class ConstantTermNormalizer from SMTInterpol to Library-SMTLIB\n* Extract method\n* Add support for new representation of bitvector constants\n  (ConstantTerm with BigInteger value)\n* Add documentation\n\nThis class is currently not used by SMTInterpol. However, this class is\nused by several projects of Ultimate, e.g., by the SMTSolverBridge.\nUltimate's projects should not depend on SMTInterpol or the SMTSolverBridge.\nHence Ultimate currently duplicates this class to make the code available\nto its projects.","shortMessageHtmlLink":"Move ConstantTermNormalizer"}},{"before":null,"after":"89eb889dde4b9502115204c592e4c6ce015df4a6","ref":"refs/heads/feature-all-smtcomp-logics","pushedAt":"2024-06-23T15:27:26.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Heizmann","name":"Matthias Heizmann","path":"/Heizmann","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1221834?s=80&v=4"},"commit":{"message":"Add QF_UFBVFP and QF_UFNIRA","shortMessageHtmlLink":"Add QF_UFBVFP and QF_UFNIRA"}},{"before":"91cb6fac2da4a6253ea04b41a7399aa5f2a09817","after":"98f115aa061342b7ff2b76b091f76de47f8335f6","ref":"refs/heads/master","pushedAt":"2024-06-17T21:30:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Report error on datatype constructor correctly.\n\nIf polymorphic function is created, but already does exists, we want to report it.\n\nFixes #105.","shortMessageHtmlLink":"Report error on datatype constructor correctly."}},{"before":"ec2a4db1284178687e9a00508290193cbdee3b08","after":"91cb6fac2da4a6253ea04b41a7399aa5f2a09817","ref":"refs/heads/master","pushedAt":"2024-06-17T20:54:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Fixed proofs of unit literal `or` in instantiation clauses.\n\nThis fixes #148","shortMessageHtmlLink":"Fixed proofs of unit literal <code>or</code> in instantiation clauses."}},{"before":"0e9bd0bf0ef211e0ad3755a8e1a802d560a30d47","after":"ec2a4db1284178687e9a00508290193cbdee3b08","ref":"refs/heads/master","pushedAt":"2024-06-14T15:48:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"last minute updates to system description","shortMessageHtmlLink":"last minute updates to system description"}},{"before":"0e9bd0bf0ef211e0ad3755a8e1a802d560a30d47","after":"ec2a4db1284178687e9a00508290193cbdee3b08","ref":"refs/heads/smtcomp2024","pushedAt":"2024-06-14T15:47:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"last minute updates to system description","shortMessageHtmlLink":"last minute updates to system description"}},{"before":null,"after":"0e9bd0bf0ef211e0ad3755a8e1a802d560a30d47","ref":"refs/heads/smtcomp2024","pushedAt":"2024-06-13T14:08:44.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Simplified some more rewrites.\n\nConstant and/or/xor.\nLogarithmic lshr.\nUse and rewrite for xor.\nNew zero/sign_extend over integer arithmetic.","shortMessageHtmlLink":"Simplified some more rewrites."}},{"before":"2c871e40079d7c8a8db19fee87c9e01945df8d82","after":"0e9bd0bf0ef211e0ad3755a8e1a802d560a30d47","ref":"refs/heads/master","pushedAt":"2024-06-13T14:06:11.000Z","pushType":"push","commitsCount":80,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Simplified some more rewrites.\n\nConstant and/or/xor.\nLogarithmic lshr.\nUse and rewrite for xor.\nNew zero/sign_extend over integer arithmetic.","shortMessageHtmlLink":"Simplified some more rewrites."}},{"before":"c7ce066d521997ee95a6123edaec7648286e56c7","after":"0e9bd0bf0ef211e0ad3755a8e1a802d560a30d47","ref":"refs/heads/Intblasting","pushedAt":"2024-06-13T14:05:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Simplified some more rewrites.\n\nConstant and/or/xor.\nLogarithmic lshr.\nUse and rewrite for xor.\nNew zero/sign_extend over integer arithmetic.","shortMessageHtmlLink":"Simplified some more rewrites."}},{"before":"d260a295a65683223cf01a4f0bc7f8cff5876754","after":"c7ce066d521997ee95a6123edaec7648286e56c7","ref":"refs/heads/Intblasting","pushedAt":"2024-06-11T10:10:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Fix bug in shift-left (use BigInteger instead of int)","shortMessageHtmlLink":"Fix bug in shift-left (use BigInteger instead of int)"}},{"before":"ab3f277d8b99caba4162b8ac96392882adac2d48","after":"d260a295a65683223cf01a4f0bc7f8cff5876754","ref":"refs/heads/Intblasting","pushedAt":"2024-06-10T17:10:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Use bv_expand_def for bitvector expand_def\n\nThe other fails the proof checker.","shortMessageHtmlLink":"Use bv_expand_def for bitvector expand_def"}},{"before":"27cf71e47bc5891fae5183eeee4bcb0f668611a5","after":"ab3f277d8b99caba4162b8ac96392882adac2d48","ref":"refs/heads/Intblasting","pushedAt":"2024-06-10T16:56:13.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Bug fix in divdiv simplification (plus new unit tests for it)","shortMessageHtmlLink":"Bug fix in divdiv simplification (plus new unit tests for it)"}},{"before":"6b606661a496762043aca17a40c68b395f8aae4c","after":"27cf71e47bc5891fae5183eeee4bcb0f668611a5","ref":"refs/heads/Intblasting","pushedAt":"2024-06-10T16:03:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Reworked bv term axioms.\n\nin addBitvectorAxioms, we only create nat2bv term and bv2nat(nat2bv) term.\nin addBv2NatAxioms, we create the axioms bv2nat(nat2bv(x))) = x mod 2^k or\n0 <= bv2nat(x) < 2^k.  (No need to state that it is in range, if it is equal\nto the mod)\nin addNat2BvAxioms, we create the nat2bv(bv2nat(x)) = x axiom or the\nnat2bv(i) = nat2bv(i mod 2^k) axiom.","shortMessageHtmlLink":"Reworked bv term axioms."}},{"before":"14bd881e67e6232b8f0886147dc5aae56e92ae89","after":"6b606661a496762043aca17a40c68b395f8aae4c","ref":"refs/heads/Intblasting","pushedAt":"2024-06-10T15:59:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Reworked bv term axioms.\n\nin addBitvectorAxioms, we only create nat2bv term and bv2nat(nat2bv) term.\nin addBv2NatAxioms, we create the axioms bv2nat(nat2bv(x))) = x mod 2^k or\n0 <= bv2nat(x) < 2^k.  (No need to state that it is in range, if it is equal\nto the mod)\nin addNat2BvAxioms, we create the nat2bv(bv2nat(x)) = x axiom or the\nnat2bv(i) = nat2bv(i mod 2^k) axiom.","shortMessageHtmlLink":"Reworked bv term axioms."}},{"before":"7aeb15a071fb9d5410b786797092afde4fb8d2e9","after":"14bd881e67e6232b8f0886147dc5aae56e92ae89","ref":"refs/heads/Intblasting","pushedAt":"2024-06-10T08:15:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Fix bug in model builder for bv.","shortMessageHtmlLink":"Fix bug in model builder for bv."}},{"before":"de02de5f873214dbcded2b9f40c8b6a978d4d8ef","after":"7aeb15a071fb9d5410b786797092afde4fb8d2e9","ref":"refs/heads/Intblasting","pushedAt":"2024-06-09T18:44:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Updated text for bitvector proof production","shortMessageHtmlLink":"Updated text for bitvector proof production"}},{"before":"c990272aac04a34b79b767049c3d3e3a30572360","after":"de02de5f873214dbcded2b9f40c8b6a978d4d8ef","ref":"refs/heads/Intblasting","pushedAt":"2024-06-09T18:26:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"SMTCOMP target updated\n\nAdded error.log, proof-check-mode for bv","shortMessageHtmlLink":"SMTCOMP target updated"}},{"before":"0d97332d1af050e7a7b95706d2b0a35fcd454586","after":"c990272aac04a34b79b767049c3d3e3a30572360","ref":"refs/heads/Intblasting","pushedAt":"2024-06-09T18:22:42.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Added bvand with constant optimization","shortMessageHtmlLink":"Added bvand with constant optimization"}},{"before":"2d96edcc23e138d84895891fec78238c292115e1","after":"0d97332d1af050e7a7b95706d2b0a35fcd454586","ref":"refs/heads/Intblasting","pushedAt":"2024-06-08T20:11:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Report unknown if model validation fails.\n\nAlso don't report the whole oracle clause, but just it's annotation.","shortMessageHtmlLink":"Report unknown if model validation fails."}},{"before":"b4a4367e3e4bcda5244c04efe72ffd52d439223c","after":"2d96edcc23e138d84895891fec78238c292115e1","ref":"refs/heads/Intblasting","pushedAt":"2024-06-08T15:22:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Proof production for BV implemented","shortMessageHtmlLink":"Proof production for BV implemented"}},{"before":"c911f924b1ea9086d2b82863251f2c75691e26aa","after":"b4a4367e3e4bcda5244c04efe72ffd52d439223c","ref":"refs/heads/Intblasting","pushedAt":"2024-06-08T00:45:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Minor simplification","shortMessageHtmlLink":"Minor simplification"}},{"before":"4831f041b5fea3cb204c4fa9a89867a4df2ca998","after":"c911f924b1ea9086d2b82863251f2c75691e26aa","ref":"refs/heads/Intblasting","pushedAt":"2024-06-08T00:42:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Added bvsmod, improved unit test","shortMessageHtmlLink":"Added bvsmod, improved unit test"}},{"before":"702b19481f82fb15c5c980249ef334648ade2d33","after":"4831f041b5fea3cb204c4fa9a89867a4df2ca998","ref":"refs/heads/Intblasting","pushedAt":"2024-06-07T21:20:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Implement chainable comparison and add test","shortMessageHtmlLink":"Implement chainable comparison and add test"}},{"before":"2ffad28258bec3aa07f9e5e7e33b6e0c0f39b03d","after":"702b19481f82fb15c5c980249ef334648ade2d33","ref":"refs/heads/Intblasting","pushedAt":"2024-06-07T20:58:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Added model-check-mode to smtcomp bv-Skript","shortMessageHtmlLink":"Added model-check-mode to smtcomp bv-Skript"}},{"before":"ad3a1d6e74340f35b8561bdf2b17a6b671e46a2f","after":"2ffad28258bec3aa07f9e5e7e33b6e0c0f39b03d","ref":"refs/heads/Intblasting","pushedAt":"2024-06-07T20:43:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Fix more unit tests","shortMessageHtmlLink":"Fix more unit tests"}},{"before":"a7249f95f7c88962ec95de2979d6e40c5166aede","after":"ad3a1d6e74340f35b8561bdf2b17a6b671e46a2f","ref":"refs/heads/Intblasting","pushedAt":"2024-06-07T20:43:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Fix unit tests and add more","shortMessageHtmlLink":"Fix unit tests and add more"}},{"before":"e581d6c7b12f4be2fd80ab6b0ed21ec73f0b7d38","after":"a7249f95f7c88962ec95de2979d6e40c5166aede","ref":"refs/heads/Intblasting","pushedAt":"2024-06-07T20:31:43.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Fix array model production.\n\nAvoid calling freshValue for finite sorts","shortMessageHtmlLink":"Fix array model production."}},{"before":"956b7f728bd114d5d43d04fb7e987f0e14a0647b","after":"e581d6c7b12f4be2fd80ab6b0ed21ec73f0b7d38","ref":"refs/heads/Intblasting","pushedAt":"2024-06-07T18:24:36.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jhoenicke","name":"Jochen Hoenicke","path":"/jhoenicke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/897826?s=80&v=4"},"commit":{"message":"Added Bitvector model production and checking","shortMessageHtmlLink":"Added Bitvector model production and checking"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNi0yM1QxNzo1MTo0OC4wMDAwMDBazwAAAARs3Ozs","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNi0wN1QxODoyNDozNi4wMDAwMDBazwAAAARffv15"}},"title":"Activity · ultimate-pa/smtinterpol"}