diff --git a/packages/z3/build.sh b/packages/z3/build.sh
index b83fa5d36..49d4201fa 100644
--- a/packages/z3/build.sh
+++ b/packages/z3/build.sh
@@ -2,9 +2,9 @@ TERMUX_PKG_HOMEPAGE=https://github.com/Z3Prover/z3
 TERMUX_PKG_DESCRIPTION="Z3 is a theorem prover from Microsoft Research."
 TERMUX_PKG_LICENSE="MIT"
 TERMUX_PKG_MAINTAINER="@termux"
-TERMUX_PKG_VERSION=4.8.9
+TERMUX_PKG_VERSION=4.8.12
 TERMUX_PKG_SRCURL=https://github.com/Z3Prover/z3/archive/z3-$TERMUX_PKG_VERSION.tar.gz
-TERMUX_PKG_SHA256=c9fd04b9b33be74fffaac3ec2bc2c320d1a4cc32e395203c55126b12a14ff3f4
+TERMUX_PKG_SHA256=e3aaefde68b839299cbc988178529535e66048398f7d083b40c69fe0da55f8b7
 TERMUX_PKG_BUILD_IN_SRC=true
 TERMUX_MAKE_PROCESSES=1
 
@@ -13,6 +13,10 @@ termux_step_configure() {
 
 	chmod +x scripts/mk_make.py
 	CXX="$CXX" CC="$CC" python${_PYTHON_VERSION} scripts/mk_make.py --prefix=$TERMUX_PREFIX --build=$TERMUX_PKG_BUILDDIR
-	sed 's%../../../../../%%g' -i Makefile
+	if $TERMUX_ON_DEVICE_BUILD; then
+		sed 's%../../../../../../../../%%g' -i Makefile
+	else
+		sed 's%../../../../../%%g' -i Makefile
+	fi
 	sed 's/\-lpthread//g' -i config.mk
 }
diff --git a/packages/z3/sat-smt-euf_solver.cpp.patch b/packages/z3/sat-smt-euf_solver.cpp.patch
new file mode 100644
index 000000000..a67011e50
--- /dev/null
+++ b/packages/z3/sat-smt-euf_solver.cpp.patch
@@ -0,0 +1,11 @@
+--- ./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();
diff --git a/packages/z3/sat-smt-euf_solver.h.patch b/packages/z3/sat-smt-euf_solver.h.patch
new file mode 100644
index 000000000..430fd763c
--- /dev/null
+++ b/packages/z3/sat-smt-euf_solver.h.patch
@@ -0,0 +1,11 @@
+--- ./src/sat/smt/euf_solver.h	2021-07-26 09:42:33.123349945 +0530
++++ ./src/sat/smt/euf_solver.h.mod	2021-07-26 09:42:55.080018799 +0530
+@@ -101,7 +101,7 @@
+         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 };
++        z3_user::solver*          m_user_propagator{ nullptr };
+         th_solver*             m_qsolver { nullptr };
+         unsigned               m_generation { 0 };
+         mutable ptr_vector<expr> m_todo;
diff --git a/packages/z3/sat-smt-user_solver.cpp.patch b/packages/z3/sat-smt-user_solver.cpp.patch
new file mode 100644
index 000000000..4bc365f1b
--- /dev/null
+++ b/packages/z3/sat-smt-user_solver.cpp.patch
@@ -0,0 +1,11 @@
+--- ./src/sat/smt/user_solver.cpp	2021-07-26 07:42:52.185967924 +0530
++++ ./src/sat/smt/user_solver.cpp.mod	2021-07-26 07:43:11.439303175 +0530
+@@ -18,7 +18,7 @@
+ #include "sat/smt/user_solver.h"
+ #include "sat/smt/euf_solver.h"
+ 
+-namespace user {
++namespace z3_user {
+ 
+     solver::solver(euf::solver& ctx) :
+         th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user"))
diff --git a/packages/z3/sat-smt-user_solver.h.patch b/packages/z3/sat-smt-user_solver.h.patch
new file mode 100644
index 000000000..f4b28678c
--- /dev/null
+++ b/packages/z3/sat-smt-user_solver.h.patch
@@ -0,0 +1,11 @@
+--- ./src/sat/smt/user_solver.h	2021-07-26 09:41:09.413341606 +0530
++++ ./src/sat/smt/user_solver.h.mod	2021-07-26 09:41:19.996675994 +0530
+@@ -23,7 +23,7 @@
+ #include "solver/solver.h"
+ 
+ 
+-namespace user {
++namespace z3_user {
+ 
+     class solver : public euf::th_euf_solver, public ::solver::propagate_callback {
+