{"action":"created","issue":{"url":"https://api.github.com/repos/sosy-lab/java-smt/issues/5","labels_url":"https://api.github.com/repos/sosy-lab/java-smt/issues/5/labels{/name}","comments_url":"https://api.github.com/repos/sosy-lab/java-smt/issues/5/comments","events_url":"https://api.github.com/repos/sosy-lab/java-smt/issues/5/events","html_url":"https://github.com/sosy-lab/java-smt/issues/5","id":120808840,"number":5,"title":"Add Visitor for Formula Traversal and Transformation","user":{"login":"PhilippWendler","id":2545335,"avatar_url":"https://avatars.githubusercontent.com/u/2545335?v=3","gravatar_id":"","url":"https://api.github.com/users/PhilippWendler","html_url":"https://github.com/PhilippWendler","followers_url":"https://api.github.com/users/PhilippWendler/followers","following_url":"https://api.github.com/users/PhilippWendler/following{/other_user}","gists_url":"https://api.github.com/users/PhilippWendler/gists{/gist_id}","starred_url":"https://api.github.com/users/PhilippWendler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/PhilippWendler/subscriptions","organizations_url":"https://api.github.com/users/PhilippWendler/orgs","repos_url":"https://api.github.com/users/PhilippWendler/repos","events_url":"https://api.github.com/users/PhilippWendler/events{/privacy}","received_events_url":"https://api.github.com/users/PhilippWendler/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"kfriedberger","id":10998542,"avatar_url":"https://avatars.githubusercontent.com/u/10998542?v=3","gravatar_id":"","url":"https://api.github.com/users/kfriedberger","html_url":"https://github.com/kfriedberger","followers_url":"https://api.github.com/users/kfriedberger/followers","following_url":"https://api.github.com/users/kfriedberger/following{/other_user}","gists_url":"https://api.github.com/users/kfriedberger/gists{/gist_id}","starred_url":"https://api.github.com/users/kfriedberger/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kfriedberger/subscriptions","organizations_url":"https://api.github.com/users/kfriedberger/orgs","repos_url":"https://api.github.com/users/kfriedberger/repos","events_url":"https://api.github.com/users/kfriedberger/events{/privacy}","received_events_url":"https://api.github.com/users/kfriedberger/received_events","type":"User","site_admin":false},"milestone":{"url":"https://api.github.com/repos/sosy-lab/java-smt/milestones/1","html_url":"https://github.com/sosy-lab/java-smt/milestones/Release%201.0","labels_url":"https://api.github.com/repos/sosy-lab/java-smt/milestones/1/labels","id":1459158,"number":1,"title":"Release 1.0","description":"","creator":{"login":"PhilippWendler","id":2545335,"avatar_url":"https://avatars.githubusercontent.com/u/2545335?v=3","gravatar_id":"","url":"https://api.github.com/users/PhilippWendler","html_url":"https://github.com/PhilippWendler","followers_url":"https://api.github.com/users/PhilippWendler/followers","following_url":"https://api.github.com/users/PhilippWendler/following{/other_user}","gists_url":"https://api.github.com/users/PhilippWendler/gists{/gist_id}","starred_url":"https://api.github.com/users/PhilippWendler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/PhilippWendler/subscriptions","organizations_url":"https://api.github.com/users/PhilippWendler/orgs","repos_url":"https://api.github.com/users/PhilippWendler/repos","events_url":"https://api.github.com/users/PhilippWendler/events{/privacy}","received_events_url":"https://api.github.com/users/PhilippWendler/received_events","type":"User","site_admin":false},"open_issues":6,"closed_issues":1,"state":"open","created_at":"2015-12-14T12:57:19Z","updated_at":"2015-12-18T16:04:49Z","due_on":null,"closed_at":null},"comments":50,"created_at":"2015-12-07T16:16:42Z","updated_at":"2015-12-22T17:27:26Z","closed_at":null,"body":"These exist already in CPAchecker and should be moved to JavaSMT."},"comment":{"url":"https://api.github.com/repos/sosy-lab/java-smt/issues/comments/166680181","html_url":"https://github.com/sosy-lab/java-smt/issues/5#issuecomment-166680181","issue_url":"https://api.github.com/repos/sosy-lab/java-smt/issues/5","id":166680181,"user":{"login":"cheshire","id":348959,"avatar_url":"https://avatars.githubusercontent.com/u/348959?v=3","gravatar_id":"","url":"https://api.github.com/users/cheshire","html_url":"https://github.com/cheshire","followers_url":"https://api.github.com/users/cheshire/followers","following_url":"https://api.github.com/users/cheshire/following{/other_user}","gists_url":"https://api.github.com/users/cheshire/gists{/gist_id}","starred_url":"https://api.github.com/users/cheshire/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cheshire/subscriptions","organizations_url":"https://api.github.com/users/cheshire/orgs","repos_url":"https://api.github.com/users/cheshire/repos","events_url":"https://api.github.com/users/cheshire/events{/privacy}","received_events_url":"https://api.github.com/users/cheshire/received_events","type":"User","site_admin":false},"created_at":"2015-12-22T17:27:26Z","updated_at":"2015-12-22T17:27:26Z","body":"> The following cases should be handled in the visitors\r\n\r\nI would actually close the feature set on boolean visitors now.\r\nWe don't need to handle every possible case. After all, SMT atoms are not really atomic, and all kinds of \"logical\" things can happen inside, and if we miss a few operators it is not a problem.\r\nThus I'm against supporting XOR, distinct and boolean variables as special cases, as it leads to even more boilerplate."}}