{"action":"created","issue":{"url":"https://api.github.com/repos/klee/klee/issues/311","labels_url":"https://api.github.com/repos/klee/klee/issues/311/labels{/name}","comments_url":"https://api.github.com/repos/klee/klee/issues/311/comments","events_url":"https://api.github.com/repos/klee/klee/issues/311/events","html_url":"https://github.com/klee/klee/pull/311","id":120517849,"number":311,"title":"Add flag to suppress errors due to infeasible assumptions.","user":{"login":"wuestholz","id":51156,"avatar_url":"https://avatars.githubusercontent.com/u/51156?v=3","gravatar_id":"","url":"https://api.github.com/users/wuestholz","html_url":"https://github.com/wuestholz","followers_url":"https://api.github.com/users/wuestholz/followers","following_url":"https://api.github.com/users/wuestholz/following{/other_user}","gists_url":"https://api.github.com/users/wuestholz/gists{/gist_id}","starred_url":"https://api.github.com/users/wuestholz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wuestholz/subscriptions","organizations_url":"https://api.github.com/users/wuestholz/orgs","repos_url":"https://api.github.com/users/wuestholz/repos","events_url":"https://api.github.com/users/wuestholz/events{/privacy}","received_events_url":"https://api.github.com/users/wuestholz/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-12-05T01:16:52Z","updated_at":"2015-12-11T14:43:19Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/klee/klee/pulls/311","html_url":"https://github.com/klee/klee/pull/311","diff_url":"https://github.com/klee/klee/pull/311.diff","patch_url":"https://github.com/klee/klee/pull/311.patch"},"body":"This adds a flag to suppress errors that are currently reported in case the condition in a `klee_assume` is infeasible. This requires fewer solver queries than branching on the condition and terminating the branch where the condition does not hold (see https://github.com/klee/klee/commit/40d9c1d6296211f8127b34036509b225b491d4b8 for helper function that implements this)."},"comment":{"url":"https://api.github.com/repos/klee/klee/issues/comments/163951951","html_url":"https://github.com/klee/klee/pull/311#issuecomment-163951951","issue_url":"https://api.github.com/repos/klee/klee/issues/311","id":163951951,"user":{"login":"ccadar","id":5022313,"avatar_url":"https://avatars.githubusercontent.com/u/5022313?v=3","gravatar_id":"","url":"https://api.github.com/users/ccadar","html_url":"https://github.com/ccadar","followers_url":"https://api.github.com/users/ccadar/followers","following_url":"https://api.github.com/users/ccadar/following{/other_user}","gists_url":"https://api.github.com/users/ccadar/gists{/gist_id}","starred_url":"https://api.github.com/users/ccadar/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ccadar/subscriptions","organizations_url":"https://api.github.com/users/ccadar/orgs","repos_url":"https://api.github.com/users/ccadar/repos","events_url":"https://api.github.com/users/ccadar/events{/privacy}","received_events_url":"https://api.github.com/users/ccadar/received_events","type":"User","site_admin":false},"created_at":"2015-12-11T14:43:19Z","updated_at":"2015-12-11T14:43:19Z","body":"Thanks, @wuestholz . This looks good to me, although I would perhaps change the help message to add \"and exit silently instead\", to make it clear that execution does not continue (e.g., by ignoring the assume). \r\n\r\nThe only other thing to do is to document this new option at http://klee.github.io/docs/options/, via the https://github.com/klee/klee.github.io repository."}}