{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":26457461,"defaultBranch":"master","name":"yices2","ownerLogin":"SRI-CSL","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-11-10T21:47:40.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/8029212?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726304011.0","currentOid":""},"activityList":{"items":[{"before":"3adb1e337324700cb8c2a77fd4403ab7722a3f79","after":null,"ref":"refs/heads/ahmed-irfan-patch-1","pushedAt":"2024-09-14T08:53:31.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"}},{"before":"c36eb74366e224bad143741e67011e276bf00d01","after":"f13608acfea891282092e5e5673452f0c777cea8","ref":"refs/heads/master","pushedAt":"2024-09-14T08:50:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"fix mcsat clause rescaling (#530)","shortMessageHtmlLink":"fix mcsat clause rescaling (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2526088209\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/530\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/530/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/530\">#530</a>)"}},{"before":null,"after":"3adb1e337324700cb8c2a77fd4403ab7722a3f79","ref":"refs/heads/ahmed-irfan-patch-1","pushedAt":"2024-09-14T08:30:25.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"fix mcsat clause rescaling","shortMessageHtmlLink":"fix mcsat clause rescaling"}},{"before":"ca0a8441771856f204e5212b3a3326be436ea52a","after":null,"ref":"refs/heads/ahmed-irfan-patch-1","pushedAt":"2024-09-11T07:37:01.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"}},{"before":"1af326bf069d03e50f3d20e786ad08e5d3f50101","after":"c36eb74366e224bad143741e67011e276bf00d01","ref":"refs/heads/master","pushedAt":"2024-09-11T07:36:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"remove duplicated code about hints in mcsat (#529)","shortMessageHtmlLink":"remove duplicated code about hints in mcsat (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2518698679\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/529\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/529/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/529\">#529</a>)"}},{"before":null,"after":"ca0a8441771856f204e5212b3a3326be436ea52a","ref":"refs/heads/ahmed-irfan-patch-1","pushedAt":"2024-09-11T06:46:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"remove duplicated code about hints in mcsat","shortMessageHtmlLink":"remove duplicated code about hints in mcsat"}},{"before":"55321b7c330c227d61a039419688fc35ef7d821a","after":"1af326bf069d03e50f3d20e786ad08e5d3f50101","ref":"refs/heads/master","pushedAt":"2024-09-10T18:20:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"karthiknukala","name":"Karthik Nukala","path":"/karthiknukala","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/25020131?s=80&v=4"},"commit":{"message":"bug in FF extension (yices_sum_component) to Yices API","shortMessageHtmlLink":"bug in FF extension (yices_sum_component) to Yices API"}},{"before":"95b84b8828258626576100a89f8dbdf14e1316f1","after":null,"ref":"refs/heads/ahmed-irfan-patch-1","pushedAt":"2024-09-08T07:25:38.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"}},{"before":"77cd0a267b0f32fdf895ef4e8cbf07bd7db901f4","after":"55321b7c330c227d61a039419688fc35ef7d821a","ref":"refs/heads/master","pushedAt":"2024-09-08T07:25:35.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Update nra_plugin.c (#528)","shortMessageHtmlLink":"Update nra_plugin.c (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2512228835\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/528\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/528/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/528\">#528</a>)"}},{"before":null,"after":"95b84b8828258626576100a89f8dbdf14e1316f1","ref":"refs/heads/ahmed-irfan-patch-1","pushedAt":"2024-09-08T06:46:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Update nra_plugin.c","shortMessageHtmlLink":"Update nra_plugin.c"}},{"before":"20e73513660f4f3d858687a81a1f3fccdeb551e1","after":null,"ref":"refs/heads/smt2-set-option-timeout","pushedAt":"2024-09-06T08:00:29.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"}},{"before":"c0a2609283b62592e6abc7be03c81957351b81b4","after":"77cd0a267b0f32fdf895ef4e8cbf07bd7db901f4","ref":"refs/heads/master","pushedAt":"2024-09-06T08:00:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"add timeout keyword to set-option in the smt2 frontend (#527)\n\n* add timeout keyword to set-option in the smt2 frontend\r\n\r\n* add timeout example","shortMessageHtmlLink":"add timeout keyword to set-option in the smt2 frontend (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2503684313\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/527\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/527/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/527\">#527</a>)"}},{"before":"1c4d70e81e2acd9c53a117dcedea4a039b5c2fa1","after":"20e73513660f4f3d858687a81a1f3fccdeb551e1","ref":"refs/heads/smt2-set-option-timeout","pushedAt":"2024-09-05T21:42:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"add timeout example","shortMessageHtmlLink":"add timeout example"}},{"before":null,"after":"1c4d70e81e2acd9c53a117dcedea4a039b5c2fa1","ref":"refs/heads/smt2-set-option-timeout","pushedAt":"2024-09-03T20:02:44.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"add timeout keyword to set-option in the smt2 frontend","shortMessageHtmlLink":"add timeout keyword to set-option in the smt2 frontend"}},{"before":"0dc2fdb865a8622ebdcd9964deada4efd95211c3","after":null,"ref":"refs/heads/ci-make-test","pushedAt":"2024-08-25T23:21:54.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"}},{"before":"e6a5726b55587913324b001aacb0ddd0e138b19c","after":"c0a2609283b62592e6abc7be03c81957351b81b4","ref":"refs/heads/master","pushedAt":"2024-08-25T23:21:51.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"run make test in CI (#524)\n\n* Update action.yml\r\n\r\n* Update windows_ci.yml\r\n\r\n* Update windows_ci.yml","shortMessageHtmlLink":"run make test in CI (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2472658406\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/524\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/524/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/524\">#524</a>)"}},{"before":"e4334113a3244c8e732b9d5452ffcdbab118c2cf","after":"0dc2fdb865a8622ebdcd9964deada4efd95211c3","ref":"refs/heads/ci-make-test","pushedAt":"2024-08-25T20:56:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Update windows_ci.yml","shortMessageHtmlLink":"Update windows_ci.yml"}},{"before":"9a44ea9b6dcf1d8339660a2d8946ca469b1e564f","after":"e4334113a3244c8e732b9d5452ffcdbab118c2cf","ref":"refs/heads/ci-make-test","pushedAt":"2024-08-25T20:36:14.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Merge branch 'master' into ci-make-test","shortMessageHtmlLink":"Merge branch 'master' into ci-make-test"}},{"before":"89c48bfa64f8e2eaed7adf40528f1a10228d8b85","after":null,"ref":"refs/heads/fix-unit-tests","pushedAt":"2024-08-25T20:36:02.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"}},{"before":"aacc130c95916891b4e235b6247186e045eab806","after":"e6a5726b55587913324b001aacb0ddd0e138b19c","ref":"refs/heads/master","pushedAt":"2024-08-25T20:35:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"fix unit tests (#525)\n\n* Update action.yml\r\n\r\n* fix unit tests\r\n\r\n* status_interrupted -> yices_status_interrupted","shortMessageHtmlLink":"fix unit tests (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2474196934\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/525\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/525/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/525\">#525</a>)"}},{"before":"984d7191eecf7dcab8ebabbe42ed9ff5c689ab3c","after":"9a44ea9b6dcf1d8339660a2d8946ca469b1e564f","ref":"refs/heads/ci-make-test","pushedAt":"2024-08-19T21:38:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Update windows_ci.yml","shortMessageHtmlLink":"Update windows_ci.yml"}},{"before":"0e4080e171d598fc64ba702a33208e80dc940ad6","after":"89c48bfa64f8e2eaed7adf40528f1a10228d8b85","ref":"refs/heads/fix-unit-tests","pushedAt":"2024-08-19T21:30:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"status_interrupted -> yices_status_interrupted","shortMessageHtmlLink":"status_interrupted -&gt; yices_status_interrupted"}},{"before":"5baccd3dc3cb8c29bc4617263f634ed10315058b","after":"0e4080e171d598fc64ba702a33208e80dc940ad6","ref":"refs/heads/fix-unit-tests","pushedAt":"2024-08-19T21:00:56.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/ci-make-test' into fix-unit-tests","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/ci-make-test' into fix-unit-tests"}},{"before":null,"after":"5baccd3dc3cb8c29bc4617263f634ed10315058b","ref":"refs/heads/fix-unit-tests","pushedAt":"2024-08-19T20:59:44.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"fix unit tests","shortMessageHtmlLink":"fix unit tests"}},{"before":null,"after":"984d7191eecf7dcab8ebabbe42ed9ff5c689ab3c","ref":"refs/heads/ci-make-test","pushedAt":"2024-08-19T07:30:58.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Update action.yml","shortMessageHtmlLink":"Update action.yml"}},{"before":"06903dad215db4f726eed6be0b49c9c1cfe7263f","after":"aacc130c95916891b4e235b6247186e045eab806","ref":"refs/heads/master","pushedAt":"2024-08-06T06:57:11.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"mcsat Random decision frequency and seed cmdline options (#522)\n\n* random dec freq and seed in the commandline\r\n\r\n* minor","shortMessageHtmlLink":"mcsat Random decision frequency and seed cmdline options (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2436871550\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/522\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/522/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/522\">#522</a>)"}},{"before":"dbfd5033054ea3836126603f8f0bb3d427502b15","after":"b8cdc3c5d44e3b5c95747569ed5f2a0cf942d277","ref":"refs/heads/rand-cmd","pushedAt":"2024-07-29T20:52:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"minor","shortMessageHtmlLink":"minor"}},{"before":null,"after":"dbfd5033054ea3836126603f8f0bb3d427502b15","ref":"refs/heads/rand-cmd","pushedAt":"2024-07-29T20:31:49.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"random dec freq and seed in the commandline","shortMessageHtmlLink":"random dec freq and seed in the commandline"}},{"before":"edc0d01db5da6f11437c9d9a31f16c8d56dfff2f","after":"06903dad215db4f726eed6be0b49c9c1cfe7263f","ref":"refs/heads/master","pushedAt":"2024-07-03T20:03:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Finite Field support (#513)\n\n* Symbols created, eval_ff_* to be done\r\n\r\n* Added ff_plugin stub\r\n\r\n* Registered ff plugin to mcsat\r\n\r\n* Added further type support for FF type\r\n\r\n* Added printing support for the ff type\r\n\r\n* fixed warning\r\n\r\n* actual missing error strings\r\n\r\n* Parsing of (as (_ ff3 13) FF0) done\r\n\r\n* reformat indentions\r\n\r\n* reformat indentions\r\n\r\n* Front-end parsing done\r\n\r\n* mod_rba_buffer_t and TAG_ARITH_FF_BUFFER\r\n\r\n* Code Formatting\r\n\r\n* Finite Field term generation done\r\n\r\n* Fixed print_elem in term_stack2.c\r\n\r\n* Code Formatting\r\n\r\n* Removed unnecessary todos\r\n\r\n* Support arbitrary finite field size\r\n\r\n* Some optimization for ff eq term generation\r\n\r\n* Code Formatting and Warning fixes\r\n\r\n* Added exceptions when ff is solved with non-mcsat context.\r\n\r\n* fixed model_eval to handle finite field terms (and return unknown).\r\n\r\n* Term manager update (added further ff code to term_manager)\r\n\r\n* Added FF support to MCSAT preprocessor\r\n\r\n* Added FF support to model printing\r\n\r\n* fix\r\n\r\n* Fixed printing and added value_ff_t.\r\n\r\n* WIP: ff_plugin_new_term_notify\r\n\r\n* Code Formatting fixes\r\n\r\n* extracted lp_data handling from NRA plugin\r\n\r\n* moved trail_variable_compare to trail and added lp_data in ff_plugin\r\n\r\n* extracted poly_constraint from nra to lp_constraint_db\r\n\r\n* fixed bug in non mcsat part\r\n\r\n* using lp_data in explanation\r\n\r\n* store term_t in lp_data instead of variable_t\r\n\r\n* Consolidated libpoly_utils.c\r\n\r\n* update nra_plugin_explain to support lp_data\r\n\r\n* fixed context_config bug\r\n\r\n* added mcsat only checks to makefile\r\n\r\n* rework done: extracted lib_poly code from nra.\r\n\r\n* rework done: extracted unit_info from nra and bv\r\n\r\n* implementation of term_notify in ff done\r\n\r\n* fixed Makefile whitespaces\r\n\r\n* ff_poly_constraint_create implemented and minor improvements in the nra plugin.\r\n\r\n* Build system update to use static libpoly for all builds when configured\r\n\r\n* fixed term printing issue\r\n\r\n* make lp_data_t finite field order aware\r\n\r\n* throw exception on multiple ff orders\r\n\r\n* extracted constraint_unit_info_demote\r\n\r\n* Fixed typos\r\n\r\n* minor code rework to enable the compiler to remove nra_plugin_check_assignment for release builds\r\n\r\n* implemented pop/push and parts of propagate\r\n\r\n* Typos and minor code fixes\r\n\r\n* Added feasible_int_set_db files\r\n\r\n* value_version_set done\r\n\r\n* Renamed to ff_feasible_set_db\r\n\r\n* Attach/Detach lp_int_ring_t in ff_feasible_set\r\n\r\n* added ff_feasible_set_db to ff_plugin\r\n\r\n* Typos and minor code fixes\r\n\r\n* ffsat propagation done\r\n\r\n* fixed two assertions\r\n\r\n* value_hash_map made first and next record operate on const value.\r\n\r\n* value_version_set fixed bugs\r\n\r\n* Implemented ff_plugin_decide and some minor fixes\r\n\r\n* Added calls to ff_feasible_set_db_pop/_push\r\n\r\n* Using new libpoly features\r\n\r\n* Fixed zero finding and some printing issues\r\n\r\n* Typos and minor code fixes\r\n\r\n* Implemented ff_plugin_explain_propagation and ff_plugin_explain_evaluation (taken from nra)\r\n\r\n* Created functions for ff explain\r\n\r\n* Typos and minor code fixes\r\n\r\n* Prepared to plug explanation in\r\n\r\n* Added explanation procedure\r\n\r\n* Update ff_plugin_explain.c to avoid polynomial copying.\r\n\r\n* Added plugin_ctx to lp_data\r\n\r\n* fixed trace printing in ff_plugin_explain\r\n\r\n* Fixed some stuff\r\n\r\n* Fixed bugs in testing\r\n\r\n* Moved some code, addes some asserts\r\n\r\n* Some optimizations\r\n\r\n* fixup\r\n\r\n* fixed some bugs\r\n\r\n* added last_reason_unsat conflict core minimization\r\n\r\n* added gc sweep in lp_data.c\r\n\r\n* added irreducible factor calculation to ff_plugin_explain.c\r\n\r\n* added common factor removal\r\n\r\n* added :dump-model option\r\n\r\n* fixed ff model printing\r\n\r\n* Typos and minor code fixes\r\n\r\n* allowed ff-1\r\n\r\n* added todos/comments/ideas\r\n\r\n* Fixed warnings in release build\r\n\r\n* added libpoly root finding\r\n\r\n* fixed duplicated function\r\n\r\n* fixed missing case in mcsat solver.c\r\n\r\n* code format\r\n\r\n* Fixed todos in explain\r\n\r\n* added debugging code\r\n\r\n* report out of memory if rb and lp don't agree\r\n\r\n* Update Readme with special build steps\r\n\r\n* Update readme\r\n\r\n* Update readme\r\n\r\n* Fixed compile warnings\r\n\r\n* Fixed compile warnings in release build.\r\n\r\n* Fixed typos\r\n\r\n* rename int_queue_t size with capacity\r\n\r\n* enhanced int_queue\r\n\r\n* added queue for next decision\r\n\r\n* Clear hint queue on conflict\r\n\r\n* Added two queues (top and hint)\r\n\r\n* fixed bug\r\n\r\n* added solver hints in NRA\r\n\r\n* model_interpolation questions\r\n\r\n* model_interpolation does not perform request_top_decision\r\n\r\n* Remove shortcut variables from the queue\r\n\r\n* regression prints execution time\r\n\r\n* nra_plugin.c hint only on real solution\r\n\r\n* variable selection forces decision on hint\r\n\r\n* fix random decision\r\n\r\n* trace printing\r\n\r\n* changed the gold of a model interpolant\r\n\r\n* added option for test issue204.smt2\r\n\r\n* Added ff regression tests\r\n\r\n* Added hint queue in ff\r\n\r\n* Added fintie field cases in substitution.c\r\n\r\n* Added const to rational functions\r\n\r\n* Made ff order (rational_t *mod) const\r\n\r\n* Some code rework and fixed missing mod calculation in arith_ff_buffer_to_term\r\n\r\n* renamed srs to lp_polynomial_subres in libpoly\r\n\r\n* removed changes to build system (align with master)\r\n\r\n* minor reworks in feasible_set_db and nra_plugin\r\n\r\n* Integrated lp_feasibility_set_int in ff_plugin\r\n\r\n* Added quickxplain to ff_feasible_set_db\r\n\r\n* Added pointer to nra_plugin in feasible_set_db\r\n\r\n* Changed the finite field logic from FF to FFA\r\n\r\n* Code Formatting fixes\r\n\r\n* Minor code cleanup\r\n\r\n* Added comment\r\n\r\n* Reverted README.md\r\n\r\n* Removed broken runtime estimate from check.sh\r\n\r\n* added more const\r\n\r\n* Fixed false-positive warning in gcc\r\n\r\n* Removed non-passing test\r\n\r\n* Removed additional check code, since issue 520 is fixed\r\n\r\n* Fixed typos\r\n\r\n* Added missing FFA in arith framgemt_names\r\n\r\n* run_test.sh: removed tailing } in filenames\r\n\r\n* Adaptions to feedback, part 1\r\n\r\n* Minor rework\r\n\r\n* Adaptions to feedback, part 2\r\n\r\n* Removed unused value_version_set\r\n\r\n* Updated FFA error printing\r\n\r\n* Update comments\r\n\r\n* fixed test gold file\r\n\r\n---------\r\n\r\nCo-authored-by: Thomas Hader <thomas.hader@sri.com>\r\nCo-authored-by: Thomas Hader <tom@hader.email>\r\nCo-authored-by: Thomas Hader <thader@drei.at>","shortMessageHtmlLink":"Finite Field support (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2315483470\" data-permission-text=\"Title is private\" data-url=\"https://github.com/SRI-CSL/yices2/issues/513\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/SRI-CSL/yices2/pull/513/hovercard\" href=\"https://github.com/SRI-CSL/yices2/pull/513\">#513</a>)"}},{"before":"d9bc6ca51da80699e9570a3374feae89c0b4a505","after":"9f786bd49d7558bf451b54a09bb6f6fdf1b23a70","ref":"refs/heads/smtcomp2024","pushedAt":"2024-06-24T07:25:16.000Z","pushType":"push","commitsCount":8,"pusher":{"login":"ahmed-irfan","name":"Ahmed Irfan","path":"/ahmed-irfan","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43099566?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/mcsat-ufnra-model-fix' into smtcomp2024","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/mcsat-ufnra-model-fix' into smtc…"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xNFQwODo1MzozMS4wMDAwMDBazwAAAAS2JCxE","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xNFQwODo1MzozMS4wMDAwMDBazwAAAAS2JCxE","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNi0yNFQwNzoyNToxNi4wMDAwMDBazwAAAARtN7t9"}},"title":"Activity · SRI-CSL/yices2"}