{"action":"reopened","issue":{"url":"https://api.github.com/repos/stp/stp/issues/293","repository_url":"https://api.github.com/repos/stp/stp","labels_url":"https://api.github.com/repos/stp/stp/issues/293/labels{/name}","comments_url":"https://api.github.com/repos/stp/stp/issues/293/comments","events_url":"https://api.github.com/repos/stp/stp/issues/293/events","html_url":"https://github.com/stp/stp/issues/293","id":339005034,"node_id":"MDU6SXNzdWUzMzkwMDUwMzQ=","number":293,"title":"option to bit-blast in CNF and call the SAT solver","user":{"login":"steseb","id":8937508,"node_id":"MDQ6VXNlcjg5Mzc1MDg=","avatar_url":"https://avatars2.githubusercontent.com/u/8937508?v=4","gravatar_id":"","url":"https://api.github.com/users/steseb","html_url":"https://github.com/steseb","followers_url":"https://api.github.com/users/steseb/followers","following_url":"https://api.github.com/users/steseb/following{/other_user}","gists_url":"https://api.github.com/users/steseb/gists{/gist_id}","starred_url":"https://api.github.com/users/steseb/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/steseb/subscriptions","organizations_url":"https://api.github.com/users/steseb/orgs","repos_url":"https://api.github.com/users/steseb/repos","events_url":"https://api.github.com/users/steseb/events{/privacy}","received_events_url":"https://api.github.com/users/steseb/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":10,"created_at":"2018-07-06T16:49:11Z","updated_at":"2018-09-14T04:45:44Z","closed_at":null,"author_association":"NONE","body":"Hello,\r\nI noticed a severe performance degradation by using STP with the cryptominisat backend in place of directly call cryptominisat. Is it possible to have an option on the binary (and on the python API) that just bit-blasts the SMT2 expressions in CNF form and then calls the SAT solver used in the backend?\r\n\r\nThanks"}}
{"actor":{"display_login":"TrevorHansen"}}