--- ./src/sat/smt/euf_solver.cpp 2021-07-13 18:55:23.000000000 +0530 +++ ./src/sat/smt/euf_solver.cpp.mod 2021-07-26 10:59:51.900088232 +0530 @@ -836,7 +836,7 @@ ::solver::push_eh_t& push_eh, ::solver::pop_eh_t& pop_eh, ::solver::fresh_eh_t& fresh_eh) { - m_user_propagator = alloc(user::solver, *this); + m_user_propagator = alloc(z3_user::solver, *this); m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh); for (unsigned i = m_scopes.size(); i-- > 0; ) m_user_propagator->push();