mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Issue #5586 reported that Android builds (targetting, e.g., x86) failed to compile due to a conflict between: * `struct user` in `sys/user.h`; and * `namespace user` in z3's `user_solver.h` This issue is resolved by renaming `namespace user` to `namespace user_solver` (matching the header name) to avoid this conflict. Reported-by: Jamie Collinson <jamiecollinson@gmail.com> Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
This commit is contained in:
parent
bfa960c2ce
commit
f1b8376739
|
@ -994,7 +994,7 @@ namespace euf {
|
|||
::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(user_solver::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();
|
||||
|
|
|
@ -101,7 +101,7 @@ namespace euf {
|
|||
sat::sat_internalizer* m_to_si;
|
||||
scoped_ptr<euf::ackerman> m_ackerman;
|
||||
scoped_ptr<sat::dual_solver> m_dual_solver;
|
||||
user::solver* m_user_propagator = nullptr;
|
||||
user_solver::solver* m_user_propagator = nullptr;
|
||||
th_solver* m_qsolver = nullptr;
|
||||
unsigned m_generation = 0;
|
||||
mutable ptr_vector<expr> m_todo;
|
||||
|
|
|
@ -18,7 +18,7 @@ Author:
|
|||
#include "sat/smt/user_solver.h"
|
||||
#include "sat/smt/euf_solver.h"
|
||||
|
||||
namespace user {
|
||||
namespace user_solver {
|
||||
|
||||
solver::solver(euf::solver& ctx) :
|
||||
th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user"))
|
||||
|
|
|
@ -23,7 +23,7 @@ Author:
|
|||
#include "solver/solver.h"
|
||||
|
||||
|
||||
namespace user {
|
||||
namespace user_solver {
|
||||
|
||||
class solver : public euf::th_euf_solver, public ::solver::propagate_callback {
|
||||
|
||||
|
|
Loading…
Reference in a new issue