{"action":"closed","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/376","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/376/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/376/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/376/events","html_url":"https://github.com/Z3Prover/z3/issues/376","id":121989762,"number":376,"title":"make error:  no matching function for call to ‘smt::theory_seq::eq::eq","user":{"login":"liuyuer","id":2366814,"avatar_url":"https://avatars.githubusercontent.com/u/2366814?v=3","gravatar_id":"","url":"https://api.github.com/users/liuyuer","html_url":"https://github.com/liuyuer","followers_url":"https://api.github.com/users/liuyuer/followers","following_url":"https://api.github.com/users/liuyuer/following{/other_user}","gists_url":"https://api.github.com/users/liuyuer/gists{/gist_id}","starred_url":"https://api.github.com/users/liuyuer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/liuyuer/subscriptions","organizations_url":"https://api.github.com/users/liuyuer/orgs","repos_url":"https://api.github.com/users/liuyuer/repos","events_url":"https://api.github.com/users/liuyuer/events{/privacy}","received_events_url":"https://api.github.com/users/liuyuer/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-12-14T07:30:26Z","updated_at":"2015-12-15T22:46:13Z","closed_at":"2015-12-15T22:46:13Z","body":"src/smt/theory_seq.cpp\r\n../src/smt/theory_seq.cpp: In member function ‘bool smt::theory_seq::simplify_eq(expr*, expr*, smt::theory_seq::enode_pair_dependency*)’:\r\n../src/smt/theory_seq.cpp:421:86: error: no matching function for call to ‘smt::theory_seq::eq::eq(expr_ref, expr_ref, smt::theory_seq::enode_pair_dependency*&)’\r\n         m_eqs.push_back(eq(expr_ref(lhs[i].get(), m), expr_ref(rhs[i].get(), m), deps));\r\n                                                                                      ^\r\n../src/smt/theory_seq.cpp:421:86: note: candidates are:\r\nIn file included from ../src/smt/theory_seq.cpp:23:0:\r\n../src/smt/theory_seq.h:103:13: note: smt::theory_seq::eq::eq(const smt::theory_seq::eq&)\r\n             eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}\r\n             ^\r\n../src/smt/theory_seq.h:103:13: note:   candidate expects 1 argument, 3 provided\r\n../src/smt/theory_seq.h:101:13: note: smt::theory_seq::eq::eq(expr_ref&, expr_ref&, smt::theory_seq::enode_pair_dependency*)\r\n             eq(expr_ref& l, expr_ref& r, enode_pair_dependency* d):\r\n             ^\r\n../src/smt/theory_seq.h:101:13: note:   no known conversion for argument 1 from ‘expr_ref {aka obj_ref<expr, ast_manager>}’ to ‘expr_ref& {aka obj_ref<expr, ast_manager>&}’\r\n../src/smt/theory_seq.cpp: In member function ‘expr_ref smt::theory_seq::expand(expr*, smt::theory_seq::enode_pair_dependency*&)’:\r\n../src/smt/theory_seq.cpp:741:46: error: no matching function for call to ‘smt::theory_seq::solution_map::add_cache(expr*&, smt::theory_seq::expr_dep)’\r\n     m_rep.add_cache(e, expr_dep(result, deps));\r\n                                              ^\r\n../src/smt/theory_seq.cpp:741:46: note: candidate is:\r\nIn file included from ../src/smt/theory_seq.cpp:23:0:\r\n../src/smt/theory_seq.h:69:19: note: void smt::theory_seq::solution_map::add_cache(expr*, smt::theory_seq::expr_dep&)\r\n             void  add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }\r\n                   ^\r\n../src/smt/theory_seq.h:69:19: note:   no known conversion for argument 2 from ‘smt::theory_seq::expr_dep {aka std::pair<expr*, dependency_manager<scoped_dependency_manager<std::pair<smt::enode*, smt::enode*> >::config>::dependency*>}’ to ‘smt::theory_seq::expr_dep& {aka std::pair<expr*, dependency_manager<scoped_dependency_manager<std::pair<smt::enode*, smt::enode*> >::config>::dependency*>&}’\r\nmake: *** [smt/theory_seq.o] Error 1\r\n"}}