{"action":"closed","issue":{"url":"https://api.github.com/repos/msoos/cryptominisat/issues/222","labels_url":"https://api.github.com/repos/msoos/cryptominisat/issues/222/labels{/name}","comments_url":"https://api.github.com/repos/msoos/cryptominisat/issues/222/comments","events_url":"https://api.github.com/repos/msoos/cryptominisat/issues/222/events","html_url":"https://github.com/msoos/cryptominisat/issues/222","id":63215345,"number":222,"title":"rhs in clean_one_xor is modified but not used","user":{"login":"msoos","id":1334841,"avatar_url":"https://avatars.githubusercontent.com/u/1334841?v=3","gravatar_id":"","url":"https://api.github.com/users/msoos","html_url":"https://github.com/msoos","followers_url":"https://api.github.com/users/msoos/followers","following_url":"https://api.github.com/users/msoos/following{/other_user}","gists_url":"https://api.github.com/users/msoos/gists{/gist_id}","starred_url":"https://api.github.com/users/msoos/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/msoos/subscriptions","organizations_url":"https://api.github.com/users/msoos/orgs","repos_url":"https://api.github.com/users/msoos/repos","events_url":"https://api.github.com/users/msoos/events{/privacy}","received_events_url":"https://api.github.com/users/msoos/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/msoos/cryptominisat/labels/bug","name":"bug","color":"fc2929"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-03-20T11:59:12Z","updated_at":"2015-08-30T00:18:40Z","closed_at":"2015-08-30T00:18:40Z","body":"This may be a bug. Maybe it should be `bool& rhs = x.rhs` ?\r\n```\r\nool Gaussian::clean_one_xor(Xor& x)\r\n{\r\n    bool rhs = x.rhs;\r\n    size_t i = 0;\r\n    size_t j = 0;\r\n    for(size_t size = x.vars.size(); i < size; i++) {\r\n        Var var = x.vars[i];\r\n        if (solver->value(i) != l_Undef) {\r\n            if (solver->value(i) == l_True) {\r\n                rhs ^= true;\r\n            }\r\n        } else {\r\n            x.vars[j++] = var;\r\n        }\r\n    }\r\n    x.vars.resize(x.vars.size()-(i-j));\r\n\r\n    switch(x.vars.size()) {\r\n        case 0:\r\n            solver->ok &= !x.rhs;\r\n            return false;\r\n\r\n        case 1: {\r\n            solver->fully_enqueue_this(Lit(x.vars[0], !x.rhs));\r\n            return false;\r\n        }\r\n        case 2: {\r\n            solver->add_xor_clause_inter(vars_to_lits(x.vars), x.rhs);\r\n            return false;\r\n        }\r\n        default: {\r\n            return true;\r\n            break;\r\n        }\r\n    }\r\n}\r\n```\r\n\r\nSubmitted through email by Andrew Coke"}}