{"action":"created","issue":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/3243","repository_url":"https://api.github.com/repos/diffblue/cbmc","labels_url":"https://api.github.com/repos/diffblue/cbmc/issues/3243/labels{/name}","comments_url":"https://api.github.com/repos/diffblue/cbmc/issues/3243/comments","events_url":"https://api.github.com/repos/diffblue/cbmc/issues/3243/events","html_url":"https://github.com/diffblue/cbmc/pull/3243","id":375013846,"node_id":"MDExOlB1bGxSZXF1ZXN0MjI2NTU4MDk2","number":3243,"title":"solvers: also link MiniSat2 options","user":{"login":"nmanthey","id":24810598,"node_id":"MDQ6VXNlcjI0ODEwNTk4","avatar_url":"https://avatars0.githubusercontent.com/u/24810598?v=4","gravatar_id":"","url":"https://api.github.com/users/nmanthey","html_url":"https://github.com/nmanthey","followers_url":"https://api.github.com/users/nmanthey/followers","following_url":"https://api.github.com/users/nmanthey/following{/other_user}","gists_url":"https://api.github.com/users/nmanthey/gists{/gist_id}","starred_url":"https://api.github.com/users/nmanthey/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nmanthey/subscriptions","organizations_url":"https://api.github.com/users/nmanthey/orgs","repos_url":"https://api.github.com/users/nmanthey/repos","events_url":"https://api.github.com/users/nmanthey/events{/privacy}","received_events_url":"https://api.github.com/users/nmanthey/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2018-10-29T13:25:23Z","updated_at":"2018-10-31T14:28:43Z","closed_at":null,"author_association":"NONE","pull_request":{"url":"https://api.github.com/repos/diffblue/cbmc/pulls/3243","html_url":"https://github.com/diffblue/cbmc/pull/3243","diff_url":"https://github.com/diffblue/cbmc/pull/3243.diff","patch_url":"https://github.com/diffblue/cbmc/pull/3243.patch"},"body":"To be able to parse options again when setting up a solver, the\r\nparseOption method has to be present. Hence, link against the\r\nOptions.cc file of MiniSat2 as well.\r\n\r\nSigned-off-by: Norbert Manthey <nmanthey@amazon.de>\r\n\r\nNote: For the current CBMC, nothing will change from a feature or performance perspective (except binary size). This change allows to exchange the existing MiniSat with other versions of that solver, especially https://github.com/conp-solutions/minisat. This fork comes with solver performance improvements, and which allows to specify SAT solver parameters via environment variable - to allow SAT solver tuning for CBMC more easily.\r\n\r\n- [x] Each commit message has a non-empty body, explaining why the change was made.\r\n- [x] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.\r\n- [x] Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).\r\n- [x] My commit message includes data points confirming performance improvements (if claimed).\r\n- [x] My PR is restricted to a single feature or bugfix.\r\n- [x] White-space or formatting changes outside the feature-related changed lines are in commits of their own."},"comment":{"url":"https://api.github.com/repos/diffblue/cbmc/issues/comments/434708282","html_url":"https://github.com/diffblue/cbmc/pull/3243#issuecomment-434708282","issue_url":"https://api.github.com/repos/diffblue/cbmc/issues/3243","id":434708282,"node_id":"MDEyOklzc3VlQ29tbWVudDQzNDcwODI4Mg==","user":{"login":"kroening","id":1830565,"node_id":"MDQ6VXNlcjE4MzA1NjU=","avatar_url":"https://avatars0.githubusercontent.com/u/1830565?v=4","gravatar_id":"","url":"https://api.github.com/users/kroening","html_url":"https://github.com/kroening","followers_url":"https://api.github.com/users/kroening/followers","following_url":"https://api.github.com/users/kroening/following{/other_user}","gists_url":"https://api.github.com/users/kroening/gists{/gist_id}","starred_url":"https://api.github.com/users/kroening/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kroening/subscriptions","organizations_url":"https://api.github.com/users/kroening/orgs","repos_url":"https://api.github.com/users/kroening/repos","events_url":"https://api.github.com/users/kroening/events{/privacy}","received_events_url":"https://api.github.com/users/kroening/received_events","type":"User","site_admin":false},"created_at":"2018-10-31T14:28:43Z","updated_at":"2018-10-31T14:28:43Z","author_association":"MEMBER","body":"Very happy to link in options.cc -- I am mostly wondering whether you can simply drop the \"diff to the diff\" for options.cc? (Also very happy to benchmark your Minisat fork, independently)."}}
{"actor":{"display_login":"kroening"}}