<pre style='margin:0'>
Herby Gillot (herbygillot) pushed a commit to branch master
in repository macports-ports.
</pre>
<p><a href="https://github.com/macports/macports-ports/commit/3ad54b3dcc2ab79a7a3eacd64f1ac0e12ba5a344">https://github.com/macports/macports-ports/commit/3ad54b3dcc2ab79a7a3eacd64f1ac0e12ba5a344</a></p>
<pre style="white-space: pre; background: #F8F8F8">The following commit(s) were added to refs/heads/master by this push:
<span style='display:block; white-space:pre;color:#404040;'> new 3ad54b3dcc2 z3: unbreak the build
</span>3ad54b3dcc2 is described below
<span style='display:block; white-space:pre;color:#808000;'>commit 3ad54b3dcc2ab79a7a3eacd64f1ac0e12ba5a344
</span>Author: barracuda156 <vital.had@gmail.com>
AuthorDate: Sun Oct 8 11:29:56 2023 +0800
<span style='display:block; white-space:pre;color:#404040;'> z3: unbreak the build
</span><span style='display:block; white-space:pre;color:#404040;'>
</span><span style='display:block; white-space:pre;color:#404040;'> Fixes: https://trac.macports.org/ticket/68001
</span><span style='display:block; white-space:pre;color:#404040;'> See: https://github.com/Z3Prover/z3/issues/6869
</span>---
math/z3/Portfile | 8 ++--
math/z3/files/patch-4.12.2-fix-linking.diff | 72 +++++++++++++++++++++++++++++
2 files changed, 77 insertions(+), 3 deletions(-)
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/z3/Portfile b/math/z3/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index ebc0a98004b..bb61ed4b2a5 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/z3/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/z3/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -21,10 +21,12 @@ if {${subport} eq "${name}-fstar"} {
</span> size 4177051
} else {
github.setup Z3Prover z3 4.12.2 z3-
<span style='display:block; white-space:pre;background:#ffe0e0;'>- revision 0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ revision 1
</span> checksums rmd160 c82388de224e325c6836fb4dc65dfcab0c01e5ab \
sha256 9f58f3710bd2094085951a75791550f547903d75fe7e2fcb373c5f03fc761b8f \
size 5401038
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ # See: https://github.com/Z3Prover/z3/issues/6869
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ patchfiles-append patch-4.12.2-fix-linking.diff
</span> }
platforms darwin freebsd
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -33,9 +35,9 @@ license MIT
</span> github.tarball_from archive
if {[vercmp ${version} "4.8.9"] >= 0} {
<span style='display:block; white-space:pre;background:#ffe0e0;'>- patchfiles libz3-static.diff
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ patchfiles-append libz3-static.diff
</span> } else {
<span style='display:block; white-space:pre;background:#ffe0e0;'>- patchfiles libz3-static-4.8.5.diff
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ patchfiles-append libz3-static-4.8.5.diff
</span> }
worksrcdir ${name}-${github.tag_prefix}${version}
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/z3/files/patch-4.12.2-fix-linking.diff b/math/z3/files/patch-4.12.2-fix-linking.diff
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 00000000000..2bf61bc2cd8
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/z3/files/patch-4.12.2-fix-linking.diff
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,72 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+See: https://github.com/Z3Prover/z3/issues/6869
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+https://github.com/Z3Prover/z3/commit/99239068baec84c16acb231182341ff1633e46ea
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+https://github.com/Z3Prover/z3/commit/79aa317af441c9ab4e4a28973f68570e7f5dc9d3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+https://github.com/Z3Prover/z3/commit/06ea765b8229ea784fe6f805379c9e508eb9fed6
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/ast/rewriter/rewriter.cpp.orig 2023-05-13 03:59:04.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/ast/rewriter/rewriter.cpp 2023-10-08 10:06:28.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -17,6 +17,8 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ --*/
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/rewriter/rewriter_def.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include "ast/rewriter/push_app_ite.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include "ast/rewriter/elim_bounds.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/ast_ll_pp.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/ast_pp.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/ast_smt2_pp.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -417,3 +419,6 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ template class rewriter_tpl<beta_reducer_cfg>;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++template class rewriter_tpl<ng_push_app_ite_cfg>;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++template class rewriter_tpl<push_app_ite_cfg>;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++template class rewriter_tpl<elim_bounds_cfg>;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/ast/normal_forms/elim_term_ite.cpp.orig 2023-05-13 03:59:04.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/ast/normal_forms/elim_term_ite.cpp 2023-10-08 10:07:13.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -18,6 +18,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ --*/
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/normal_forms/elim_term_ite.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/ast_smt2_pp.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include "ast/rewriter/rewriter_def.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if (!m.is_term_ite(f)) {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -38,3 +39,4 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ return BR_DONE;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++template class rewriter_tpl<elim_term_ite_cfg>;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/ast/rewriter/elim_bounds.cpp.orig 2023-05-13 03:59:04.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/ast/rewriter/elim_bounds.cpp 2023-10-08 10:09:12.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -17,11 +17,9 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ --*/
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-#ifndef ELIM_BOUNDS_H_
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-#define ELIM_BOUNDS_H_
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/used_vars.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "util/obj_hashtable.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include "ast/rewriter/rewriter_def.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/rewriter/var_subst.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/rewriter/elim_bounds.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/ast_pp.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -199,5 +197,3 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ TRACE("elim_bounds", tout << mk_pp(q, m) << "\n" << result << "\n";);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ return true;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-#endif /* ELIM_BOUNDS_H_ */
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/ast/rewriter/push_app_ite.cpp.orig 2023-05-13 03:59:04.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/ast/rewriter/push_app_ite.cpp 2023-10-08 10:13:54.000000000 +0800
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -18,6 +18,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ --*/
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/rewriter/push_app_ite.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include "ast/rewriter/rewriter_def.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "ast/ast_pp.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span></pre><pre style='margin:0'>
</pre>