From f0ab25d2bb255352736c704135ff1aec6ff3506f Mon Sep 17 00:00:00 2001
From: "Andrew V. Jones" <andrewvaughanj@gmail.com>
Date: Sat, 9 Oct 2021 20:53:05 +0100
Subject: [PATCH] Rename 'user' to 'user_solver #5586

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>
---
 src/sat/smt/euf_solver.cpp  | 2 +-
 src/sat/smt/euf_solver.h    | 2 +-
 src/sat/smt/user_solver.cpp | 2 +-
 src/sat/smt/user_solver.h   | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 3c3b6e884ff..3c1831c8733 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -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();
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 6d08ba51222..2449335d192 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -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;
diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp
index e9d8a54cb89..5a1a07f115a 100644
--- a/src/sat/smt/user_solver.cpp
+++ b/src/sat/smt/user_solver.cpp
@@ -18,7 +18,7 @@ Module Name:
 #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"))
diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h
index e16eb5b5e6e..2939a2f0a1d 100644
--- a/src/sat/smt/user_solver.h
+++ b/src/sat/smt/user_solver.h
@@ -23,7 +23,7 @@ Module Name:
 #include "solver/solver.h"
 
 
-namespace user {
+namespace user_solver {
 
     class solver : public euf::th_euf_solver, public ::solver::propagate_callback {