Index: head/math/z3/Makefile
===================================================================
--- head/math/z3/Makefile
+++ head/math/z3/Makefile
@@ -2,10 +2,10 @@
 
 PORTNAME=	z3
 DISTVERSIONPREFIX=	${PORTNAME}-
-DISTVERSION=	4.6.0
+DISTVERSION=	4.7.1
 CATEGORIES=	math
 
-MAINTAINER=	6yearold@gmail.com
+MAINTAINER=	arrowd@FreeBSD.org
 COMMENT=	Z3 Theorem Prover
 
 LICENSE=	MIT
Index: head/math/z3/distinfo
===================================================================
--- head/math/z3/distinfo
+++ head/math/z3/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1516713093
-SHA256 (Z3Prover-z3-z3-4.6.0_GH0.tar.gz) = 511da31d1f985cf0c79b2de05bda4e057371ba519769d1546ff71e1304fe53c9
-SIZE (Z3Prover-z3-z3-4.6.0_GH0.tar.gz) = 3987830
+TIMESTAMP = 1529241358
+SHA256 (Z3Prover-z3-z3-4.7.1_GH0.tar.gz) = a353e3da00cdaffd258052cc1406efc854606855222ab4bfd5679c58af5c11c7
+SIZE (Z3Prover-z3-z3-4.7.1_GH0.tar.gz) = 4015416
Index: head/math/z3/files/patch-src_util_lp_lp__solver__instances.cpp
===================================================================
--- head/math/z3/files/patch-src_util_lp_lp__solver__instances.cpp
+++ head/math/z3/files/patch-src_util_lp_lp__solver__instances.cpp
@@ -1,11 +0,0 @@
---- src/util/lp/lp_solver_instances.cpp.orig	2018-01-23 13:13:30 UTC
-+++ src/util/lp/lp_solver_instances.cpp
-@@ -34,6 +34,8 @@ template void lp::lp_solver<double, doub
- template bool lp::lp_solver<double, double>::problem_is_empty();
- template void lp::lp_solver<double, double>::scale();
- template void lp::lp_solver<double, double>::set_scaled_cost(unsigned int);
-+template std::string lp::lp_solver<double, double>::get_column_name(unsigned int) const;
-+template std::string lp::lp_solver<rational, rational>::get_column_name(unsigned int) const;
- template lp::lp_solver<double, double>::~lp_solver();
- template void lp::lp_solver<lp::mpq, lp::mpq>::add_constraint(lp::lp_relation, lp::mpq, unsigned int);
- template void lp::lp_solver<lp::mpq, lp::mpq>::cleanup();