Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Build error on Android targets other than arm64-v8a #5586

Closed
jamiecollinson opened this issue Oct 9, 2021 · 9 comments
Closed

Build error on Android targets other than arm64-v8a #5586

jamiecollinson opened this issue Oct 9, 2021 · 9 comments

Comments

@jamiecollinson
Copy link
Contributor

I'm trying to build Z3 with java bindings for use in an Android project. I've successfully compiled for arm64-v8a with the cmake config in this script, but when I try for other targets (I'd ideally like armeabi-v7a, x86 and x86_64 so that I can build the project for all common Android devices) I get the following errors, apologies for long log, thought it would probably be helpful:

$ ../z3build.sh 
-- Android: Targeting API '21' with architecture 'x86', ABI 'x86', and processor 'i686'
-- Android: Selected unified Clang toolchain
-- The CXX compiler identification is Clang 12.0.5
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/clang++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Z3 version 4.8.13.0
-- Found simple git working directory
-- Found git directory "/Users/jamie/work/z3/.git"
-- Adding git dependency "/Users/jamie/work/z3/.git/HEAD"
-- Adding git dependency "/Users/jamie/work/z3/.git/refs/heads/master"
-- Found Git: /usr/bin/git (found version "2.17.2 (Apple Git-113)") 
-- Using Git hash in version output: c0c3e685e7801c7d670c11613f3cc8f4b293c724
-- Using Git description in version output: z3-4.8.4-5503-gc0c3e685e
-- CMake generator: Unix Makefiles
-- Build type: Release
-- Found PythonInterp: /usr/bin/python (found version "2.7.16") 
-- PYTHON_EXECUTABLE: /usr/bin/python
-- Detected target architecture: i686
-- Platform: Android
-- Not using libgmp
-- Not using Z3_API_LOG_SYNC
-- Thread-safe build
-- Performing Test HAS_SSE2
-- Performing Test HAS_SSE2 - Success
-- Looking for C++ include pthread.h
-- Looking for C++ include pthread.h - found
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD
-- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Failed
-- Check if compiler accepts -pthread
-- Check if compiler accepts -pthread - yes
-- Found Threads: TRUE  
-- Performing Test HAS__Wall
-- Performing Test HAS__Wall - Success
-- C++ compiler supports -Wall
-- Treating only serious compiler warnings as errors
-- Performing Test HAS__Werror_odr
-- Performing Test HAS__Werror_odr - Success
-- C++ compiler supports -Werror=odr
-- Performing Test HAS__Werror_delete_non_virtual_dtor
-- Performing Test HAS__Werror_delete_non_virtual_dtor - Success
-- C++ compiler supports -Werror=delete-non-virtual-dtor
-- Performing Test HAS__Werror_overloaded_virtual
-- Performing Test HAS__Werror_overloaded_virtual - Success
-- C++ compiler supports -Werror=overloaded-virtual
-- Performing Test HAS__fvisibility_hidden
-- Performing Test HAS__fvisibility_hidden - Success
-- C++ compiler supports -fvisibility=hidden
-- Performing Test HAS__fvisibility_inlines_hidden
-- Performing Test HAS__fvisibility_inlines_hidden - Success
-- C++ compiler supports -fvisibility-inlines-hidden
-- Performing Test HAS__fPIC
-- Performing Test HAS__fPIC - Success
-- C++ compiler supports -fPIC
-- LTO disabled
-- CMAKE_CXX_FLAGS: " -Werror=odr  -Werror=delete-non-virtual-dtor  -Werror=overloaded-virtual "
-- CMAKE_EXE_LINKER_FLAGS: "-Wl,--build-id=sha1 -Wl,--no-rosegment -Wl,--fatal-warnings -Qunused-arguments -Wl,--no-undefined  -Wl,--gc-sections"
-- CMAKE_STATIC_LINKER_FLAGS: ""
-- CMAKE_SHARED_LINKER_FLAGS: "-Wl,--build-id=sha1 -Wl,--no-rosegment -Wl,--fatal-warnings -Qunused-arguments -Wl,--no-undefined"
-- CMAKE_CXX_FLAGS_RELEASE: "-O3 -DNDEBUG"
-- CMAKE_EXE_LINKER_FLAGS_RELEASE: ""
-- CMAKE_SHARED_LINKER_FLAGS_RELEASE: ""
-- CMAKE_STATIC_LINKER_FLAGS_RELEASE: ""
-- Z3_COMPONENT_CXX_DEFINES: $<$<CONFIG:Debug>:Z3DEBUG>;$<$<CONFIG:Release>:_EXTERNAL_RELEASE>;$<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEASE>;-D_ANDROID_;-D_MP_INTERNAL;$<$<CONFIG:Debug>:_TRACE>
-- Z3_COMPONENT_CXX_FLAGS: -mfpmath=sse;-msse;-msse2;-Wall;-fvisibility=hidden;-fvisibility-inlines-hidden;-fPIC
-- Z3_DEPENDENT_LIBS: Threads::Threads
-- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: /Users/jamie/work/z3/build/x86/src;/Users/jamie/work/z3/src
-- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: 
-- CMAKE_INSTALL_LIBDIR: "lib"
-- CMAKE_INSTALL_BINDIR: "bin"
-- CMAKE_INSTALL_INCLUDEDIR: "include"
-- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig"
-- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3"
-- Adding component util
-- Adding component polynomial
-- Adding rule to generate "algebraic_params.hpp"
-- Adding component dd
-- Adding component hilbert
-- Adding component simplex
-- Adding component automata
-- Adding component interval
-- Adding component realclosure
-- Adding rule to generate "rcf_params.hpp"
-- Adding component subpaving
-- Adding component ast
-- Adding rule to generate "pp_params.hpp"
-- Adding component params
-- Adding rule to generate "arith_rewriter_params.hpp"
-- Adding rule to generate "array_rewriter_params.hpp"
-- Adding rule to generate "bool_rewriter_params.hpp"
-- Adding rule to generate "bv_rewriter_params.hpp"
-- Adding rule to generate "fpa_rewriter_params.hpp"
-- Adding rule to generate "fpa2bv_rewriter_params.hpp"
-- Adding rule to generate "pattern_inference_params_helper.hpp"
-- Adding rule to generate "poly_rewriter_params.hpp"
-- Adding rule to generate "rewriter_params.hpp"
-- Adding rule to generate "seq_rewriter_params.hpp"
-- Adding component rewriter
-- Adding component normal_forms
-- Adding rule to generate "nnf_params.hpp"
-- Adding component macros
-- Adding component model
-- Adding rule to generate "model_evaluator_params.hpp"
-- Adding rule to generate "model_params.hpp"
-- Adding component tactic
-- Adding rule to generate "tactic_params.hpp"
-- Adding component substitution
-- Adding component euf
-- Adding component smt_params
-- Adding rule to generate "smt_params_helper.hpp"
-- Adding component parser_util
-- Adding rule to generate "parser_params.hpp"
-- Adding component grobner
-- Adding component sat
-- Adding rule to generate "sat_asymm_branch_params.hpp"
-- Adding rule to generate "sat_params.hpp"
-- Adding rule to generate "sat_scc_params.hpp"
-- Adding rule to generate "sat_simplifier_params.hpp"
-- Adding component nlsat
-- Adding rule to generate "nlsat_params.hpp"
-- Adding component core_tactics
-- Adding component subpaving_tactic
-- Adding component aig_tactic
-- Adding component arith_tactics
-- Adding component solver
-- Adding rule to generate "combined_solver_params.hpp"
-- Adding rule to generate "parallel_params.hpp"
-- Adding rule to generate "solver_params.hpp"
-- Adding component cmd_context
-- Adding component extra_cmds
-- Adding component smt2parser
-- Adding component solver_assertions
-- Adding component pattern
-- Adding component bit_blaster
-- Adding component lp
-- Adding component mbp
-- Adding component sat_smt
-- Adding component sat_tactic
-- Adding component nlsat_tactic
-- Adding component ackermannization
-- Adding rule to generate "ackermannization_params.hpp"
-- Adding rule to generate "ackermannize_bv_tactic_params.hpp"
-- Adding component proofs
-- Adding component fpa
-- Adding component proto_model
-- Adding component smt
-- Adding component bv_tactics
-- Adding component smt_tactic
-- Adding component sls_tactic
-- Adding rule to generate "sls_params.hpp"
-- Adding component qe
-- Adding component muz
-- Adding rule to generate "fp_params.hpp"
-- Adding component dataflow
-- Adding component transforms
-- Adding component rel
-- Adding component clp
-- Adding component tab
-- Adding component bmc
-- Adding component ddnf
-- Adding component spacer
-- Adding component fp
-- Adding component ufbv_tactic
-- Adding component sat_solver
-- Adding component smtlogic_tactics
-- Adding rule to generate "qfufbv_tactic_params.hpp"
-- Adding component fpa_tactics
-- Adding component fd_solver
-- Adding component portfolio
-- Adding component opt
-- Adding rule to generate "opt_params.hpp"
-- Adding component api
-- Adding component api_dll
-- Adding component fuzzing
-- Found Java: /Applications/Android Studio Preview.app/Contents/jre/Contents/Home/bin/java (found version "11.0.10") 
-- Found JNI: /Users/jamie/work/z3/build/x86/NotNeeded  
-- Building documentation disabled
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/jamie/work/z3/build/x86
[  0%] Building CXX object src/util/CMakeFiles/util.dir/approx_nat.cpp.o
[  0%] Generating "/Users/jamie/work/z3/build/x86/src/api/java/Native.java" and "/Users/jamie/work/z3/build/x86/src/api/java/Native.cpp"
[  0%] Generating com.microsoft.z3.enumerations package
[  0%] Building CXX object src/util/CMakeFiles/util.dir/approx_set.cpp.o
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_lbool.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_symbol_kind.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_parameter_kind.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_sort_kind.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_ast_kind.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_decl_kind.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_param_kind.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_ast_print_mode.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_error_code.java"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/api/java/enumerations/Z3_goal_prec.java"
[  0%] Building CXX object src/util/CMakeFiles/util.dir/bit_util.cpp.o
Faking emission of 'api_log_macros.h'
Faking emission of 'api_log_macros.cpp'
Faking emission of 'api_commands.cpp'
Faking emission of 'z3/z3core.py'
Generated '<fdopen>'
Generated '<fdopen>'
Generated '<fdopen>'
Generated '<fdopen>'
Generated '/Users/jamie/work/z3/build/x86/src/api/java/Native.java'
[  0%] Building Java objects for z3JavaJar.jar
[  0%] Building CXX object src/util/CMakeFiles/util.dir/bit_vector.cpp.o
[  0%] Building CXX object src/util/CMakeFiles/util.dir/cmd_context_types.cpp.o
[  0%] Building CXX object src/util/CMakeFiles/util.dir/common_msgs.cpp.o
[  0%] Building CXX object src/util/CMakeFiles/util.dir/debug.cpp.o
[  0%] Building CXX object src/util/CMakeFiles/util.dir/env_params.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/fixed_bit_vector.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/gparams.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/hash.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/hwf.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/inf_int_rational.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/inf_rational.cpp.o
[  1%] Generating CMakeFiles/z3JavaJar.dir/java_class_filelist
[  1%] Creating Java archive com.microsoft.z3-4.8.13.0.jar
[  1%] Building CXX object src/util/CMakeFiles/util.dir/inf_s_integer.cpp.o
[  1%] Built target z3JavaJar
[  1%] Building CXX object src/util/CMakeFiles/util.dir/lbool.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/luby.cpp.o
[  1%] Building CXX object src/util/CMakeFiles/util.dir/memory_manager.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/min_cut.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpbq.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpf.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpff.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpfx.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpn.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpq.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpq_inf.cpp.o
[  2%] Building CXX object src/util/CMakeFiles/util.dir/mpz.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/page.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/params.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/permutation.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/prime_generator.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/rational.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/region.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/rlimit.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/scoped_ctrl_c.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/scoped_timer.cpp.o
[  3%] Building CXX object src/util/CMakeFiles/util.dir/sexpr.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/s_integer.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/small_object_allocator.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/smt2_util.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/state_graph.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/stack.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/statistics.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/symbol.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/timeit.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/timeout.cpp.o
[  4%] Building CXX object src/util/CMakeFiles/util.dir/trace.cpp.o
[  5%] Building CXX object src/util/CMakeFiles/util.dir/util.cpp.o
[  5%] Building CXX object src/util/CMakeFiles/util.dir/warning.cpp.o
[  5%] Building CXX object src/util/CMakeFiles/util.dir/z3_exception.cpp.o
[  5%] Building CXX object src/util/CMakeFiles/util.dir/zstring.cpp.o
[  5%] Built target util
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/params/seq_rewriter_params.hpp" from "seq_rewriter_params.pyg"
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/math/polynomial/algebraic_params.hpp" from "algebraic_params.pyg"
[  5%] Building CXX object src/math/dd/CMakeFiles/dd.dir/dd_bdd.cpp.o
[  5%] Building CXX object src/math/automata/CMakeFiles/automata.dir/automaton.cpp.o
INFO:root:Using /Users/jamie/work/z3/src/params/seq_rewriter_params.pyg
INFO:root:Using /Users/jamie/work/z3/src/math/polynomial/algebraic_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/seq_rewriter_params.hpp"
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/math/polynomial/algebraic_params.hpp"
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/params/arith_rewriter_params.hpp" from "arith_rewriter_params.pyg"
[  5%] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/algebraic_numbers.cpp.o
INFO:root:Using /Users/jamie/work/z3/src/params/arith_rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/arith_rewriter_params.hpp"
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/params/array_rewriter_params.hpp" from "array_rewriter_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/array_rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/array_rewriter_params.hpp"
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/params/bool_rewriter_params.hpp" from "bool_rewriter_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/bool_rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/bool_rewriter_params.hpp"
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/params/bv_rewriter_params.hpp" from "bv_rewriter_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/bv_rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/bv_rewriter_params.hpp"
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/params/fpa2bv_rewriter_params.hpp" from "fpa2bv_rewriter_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/fpa2bv_rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/fpa2bv_rewriter_params.hpp"
[  5%] Generating "/Users/jamie/work/z3/build/x86/src/params/fpa_rewriter_params.hpp" from "fpa_rewriter_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/fpa_rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/fpa_rewriter_params.hpp"
[  7%] Generating "/Users/jamie/work/z3/build/x86/src/params/pattern_inference_params_helper.hpp" from "pattern_inference_params_helper.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/pattern_inference_params_helper.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/pattern_inference_params_helper.hpp"
[  7%] Generating "/Users/jamie/work/z3/build/x86/src/params/poly_rewriter_params.hpp" from "poly_rewriter_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/poly_rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/poly_rewriter_params.hpp"
[  7%] Generating "/Users/jamie/work/z3/build/x86/src/params/rewriter_params.hpp" from "rewriter_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/params/rewriter_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/params/rewriter_params.hpp"
[  7%] Building CXX object src/params/CMakeFiles/params.dir/pattern_inference_params.cpp.o
[  7%] Building CXX object src/params/CMakeFiles/params.dir/context_params.cpp.o
[  7%] Built target automata
[  7%] Building CXX object src/math/dd/CMakeFiles/dd.dir/dd_pdd.cpp.o
[  7%] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/polynomial_cache.cpp.o
[  7%] Built target params
[  7%] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/polynomial.cpp.o
[  7%] Building CXX object src/math/simplex/CMakeFiles/simplex.dir/simplex.cpp.o
[  7%] Generating "/Users/jamie/work/z3/build/x86/src/smt/params/smt_params_helper.hpp" from "smt_params_helper.pyg"
INFO:root:Using /Users/jamie/work/z3/src/smt/params/smt_params_helper.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/smt/params/smt_params_helper.hpp"
[  7%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/dyn_ack_params.cpp.o
[  7%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/preprocessor_params.cpp.o
[  7%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/qi_params.cpp.o
[  7%] Built target dd
[  7%] Building CXX object src/math/simplex/CMakeFiles/simplex.dir/model_based_opt.cpp.o
[  7%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/smt_params.cpp.o
[  7%] Building CXX object src/math/hilbert/CMakeFiles/hilbert.dir/hilbert_basis.cpp.o
[  7%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/theory_arith_params.cpp.o
[  7%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/theory_array_params.cpp.o
[  7%] Building CXX object src/math/simplex/CMakeFiles/simplex.dir/bit_matrix.cpp.o
[  8%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/theory_bv_params.cpp.o
[  8%] Built target simplex
[  8%] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/rpolynomial.cpp.o
[  8%] Built target hilbert
[  8%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/theory_pb_params.cpp.o
[  9%] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/sexpr2upolynomial.cpp.o
[  9%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/theory_seq_params.cpp.o
[  9%] Building CXX object src/math/interval/CMakeFiles/interval.dir/interval_mpq.cpp.o
[  9%] Building CXX object src/smt/params/CMakeFiles/smt_params.dir/theory_str_params.cpp.o
[  9%] Building CXX object src/math/interval/CMakeFiles/interval.dir/dep_intervals.cpp.o
[  9%] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/upolynomial.cpp.o
[  9%] Built target smt_params
[  9%] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/upolynomial_factorization.cpp.o
[  9%] Built target interval
[  9%] Generating "/Users/jamie/work/z3/build/x86/src/math/realclosure/rcf_params.hpp" from "rcf_params.pyg"
[  9%] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving.cpp.o
INFO:root:Using /Users/jamie/work/z3/src/math/realclosure/rcf_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/math/realclosure/rcf_params.hpp"
[  9%] Building CXX object src/math/realclosure/CMakeFiles/realclosure.dir/mpz_matrix.cpp.o
[  9%] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_hwf.cpp.o
[  9%] Building CXX object src/math/realclosure/CMakeFiles/realclosure.dir/realclosure.cpp.o
[  9%] Built target polynomial
[  9%] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpf.cpp.o
[  9%] Generating "/Users/jamie/work/z3/build/x86/src/ast/pp_params.hpp" from "pp_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/ast/pp_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/ast/pp_params.hpp"
[  9%] Building CXX object src/ast/CMakeFiles/ast.dir/act_cache.cpp.o
[ 10%] Building CXX object src/ast/CMakeFiles/ast.dir/arith_decl_plugin.cpp.o
[ 10%] Building CXX object src/ast/CMakeFiles/ast.dir/array_decl_plugin.cpp.o
[ 10%] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpff.cpp.o
[ 11%] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpfx.cpp.o
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast.cpp.o
[ 11%] Built target realclosure
[ 11%] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpq.cpp.o
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_ll_pp.cpp.o
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_lt.cpp.o
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_pp_util.cpp.o
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_printer.cpp.o
[ 11%] Built target subpaving
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_smt2_pp.cpp.o
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_smt_pp.cpp.o
[ 11%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_pp_dot.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_translation.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/ast_util.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/bv_decl_plugin.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/char_decl_plugin.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/cost_evaluator.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/datatype_decl_plugin.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/decl_collector.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/display_dimacs.cpp.o
[ 13%] Building CXX object src/ast/CMakeFiles/ast.dir/dl_decl_plugin.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/expr2polynomial.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/expr2var.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/expr_abstract.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/expr_functors.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/expr_map.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/expr_stat.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/expr_substitution.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/for_each_ast.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/for_each_expr.cpp.o
[ 14%] Building CXX object src/ast/CMakeFiles/ast.dir/format.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/fpa_decl_plugin.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/func_decl_dependencies.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/has_free_vars.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/macro_substitution.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/num_occurs.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/occurs.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/pb_decl_plugin.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/pp.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/quantifier_stat.cpp.o
[ 15%] Building CXX object src/ast/CMakeFiles/ast.dir/recfun_decl_plugin.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/reg_decl_plugins.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/seq_decl_plugin.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/shared_occs.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/special_relations_decl_plugin.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/static_features.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/used_vars.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/value_generator.cpp.o
[ 16%] Building CXX object src/ast/CMakeFiles/ast.dir/well_sorted.cpp.o
[ 16%] Built target ast
[ 16%] Generating "/Users/jamie/work/z3/build/x86/src/parsers/util/parser_params.hpp" from "parser_params.pyg"
[ 16%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/arith_rewriter.cpp.o
[ 16%] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_enode.cpp.o
[ 16%] Building CXX object src/math/grobner/CMakeFiles/grobner.dir/grobner.cpp.o
INFO:root:Using /Users/jamie/work/z3/src/parsers/util/parser_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/parsers/util/parser_params.hpp"
[ 16%] Building CXX object src/parsers/util/CMakeFiles/parser_util.dir/cost_parser.cpp.o
[ 17%] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_etable.cpp.o
[ 17%] Building CXX object src/parsers/util/CMakeFiles/parser_util.dir/pattern_validation.cpp.o
[ 17%] Building CXX object src/parsers/util/CMakeFiles/parser_util.dir/scanner.cpp.o
[ 17%] Building CXX object src/math/grobner/CMakeFiles/grobner.dir/pdd_simplifier.cpp.o
[ 17%] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_egraph.cpp.o
[ 19%] Building CXX object src/parsers/util/CMakeFiles/parser_util.dir/simple_parser.cpp.o
[ 19%] Building CXX object src/math/grobner/CMakeFiles/grobner.dir/pdd_solver.cpp.o
[ 19%] Built target euf
[ 19%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/array_rewriter.cpp.o
[ 19%] Built target parser_util
[ 19%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/ast_counter.cpp.o
[ 19%] Building CXX object src/test/fuzzing/CMakeFiles/fuzzing.dir/expr_delta.cpp.o
[ 19%] Built target grobner
[ 19%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bit2int.cpp.o
[ 19%] Building CXX object src/test/fuzzing/CMakeFiles/fuzzing.dir/expr_rand.cpp.o
[ 19%] Generating "/Users/jamie/work/z3/build/x86/src/sat/sat_simplifier_params.hpp" from "sat_simplifier_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/sat/sat_simplifier_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/sat/sat_simplifier_params.hpp"
[ 19%] Generating "/Users/jamie/work/z3/build/x86/src/sat/sat_asymm_branch_params.hpp" from "sat_asymm_branch_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/sat/sat_asymm_branch_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/sat/sat_asymm_branch_params.hpp"
[ 19%] Generating "/Users/jamie/work/z3/build/x86/src/sat/sat_params.hpp" from "sat_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/sat/sat_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/sat/sat_params.hpp"
[ 19%] Generating "/Users/jamie/work/z3/build/x86/src/sat/sat_scc_params.hpp" from "sat_scc_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/sat/sat_scc_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/sat/sat_scc_params.hpp"
[ 19%] Building CXX object src/sat/CMakeFiles/sat.dir/dimacs.cpp.o
[ 20%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_aig_cuts.cpp.o
[ 20%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bool_rewriter.cpp.o
[ 20%] Built target fuzzing
[ 20%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_aig_finder.cpp.o
[ 20%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bv_bounds.cpp.o
[ 21%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bv_elim.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_anf_simplifier.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_asymm_branch.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_bcd.cpp.o
[ 21%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bv_rewriter.cpp.o
[ 21%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/cached_var_subst.cpp.o
[ 21%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/datatype_rewriter.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_big.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_binspr.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_clause.cpp.o
[ 21%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/der.cpp.o
[ 21%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/distribute_forall.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_clause_set.cpp.o
[ 21%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_clause_use_list.cpp.o
[ 22%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_cleaner.cpp.o
[ 22%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/dl_rewriter.cpp.o
[ 22%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_config.cpp.o
[ 22%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/elim_bounds.cpp.o
[ 22%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_cut_simplifier.cpp.o
[ 22%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_cutset.cpp.o
[ 22%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/enum2bv_rewriter.cpp.o
[ 22%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_ddfw.cpp.o
[ 22%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/expr_replacer.cpp.o
[ 22%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_drat.cpp.o
[ 23%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/expr_safe_replace.cpp.o
[ 23%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_elim_eqs.cpp.o
[ 23%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_elim_vars.cpp.o
[ 23%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/factor_equivs.cpp.o
[ 23%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_gc.cpp.o
[ 23%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/factor_rewriter.cpp.o
[ 23%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/fpa_rewriter.cpp.o
[ 23%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_integrity_checker.cpp.o
[ 23%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/func_decl_replace.cpp.o
[ 25%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_local_search.cpp.o
[ 25%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_lookahead.cpp.o
[ 25%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/hoist_rewriter.cpp.o
[ 25%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_lut_finder.cpp.o
[ 25%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/inj_axiom.cpp.o
[ 25%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_model_converter.cpp.o
[ 25%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/label_rewriter.cpp.o
[ 25%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/maximize_ac_sharing.cpp.o
[ 25%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/mk_simplified_app.cpp.o
[ 25%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_mus.cpp.o
[ 25%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_npn3_finder.cpp.o
[ 25%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_parallel.cpp.o
[ 26%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/pb_rewriter.cpp.o
[ 26%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/pb2bv_rewriter.cpp.o
[ 26%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/push_app_ite.cpp.o
[ 26%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_prob.cpp.o
[ 26%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_probing.cpp.o
[ 26%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_scc.cpp.o
[ 26%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/quant_hoist.cpp.o
[ 26%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/recfun_rewriter.cpp.o
[ 27%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_simplifier.cpp.o
[ 27%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/rewriter.cpp.o
[ 27%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_axioms.cpp.o
[ 27%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_solver.cpp.o
/Users/jamie/work/z3/src/sat/sat_solver.cpp:1896:22: warning: unused variable 'trail_size' [-Wunused-variable]
            unsigned trail_size = m_trail.size();
                     ^
[ 27%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_watched.cpp.o
[ 27%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_eq_solver.cpp.o
[ 27%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_rewriter.cpp.o
[ 28%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_skolem.cpp.o
[ 28%] Building CXX object src/sat/CMakeFiles/sat.dir/sat_xor_finder.cpp.o
[ 28%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/th_rewriter.cpp.o
[ 28%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/value_sweep.cpp.o
1 warning generated.
[ 28%] Built target sat
[ 28%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/var_subst.cpp.o
[ 28%] Generating "/Users/jamie/work/z3/build/x86/src/nlsat/nlsat_params.hpp" from "nlsat_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/nlsat/nlsat_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/nlsat/nlsat_params.hpp"
[ 28%] Building CXX object src/nlsat/CMakeFiles/nlsat.dir/nlsat_clause.cpp.o
[ 28%] Building CXX object src/nlsat/CMakeFiles/nlsat.dir/nlsat_evaluator.cpp.o
[ 28%] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/mk_extract_proc.cpp.o
[ 28%] Building CXX object src/nlsat/CMakeFiles/nlsat.dir/nlsat_explain.cpp.o
[ 28%] Building CXX object src/nlsat/CMakeFiles/nlsat.dir/nlsat_interval_set.cpp.o
[ 28%] Building CXX object src/nlsat/CMakeFiles/nlsat.dir/nlsat_solver.cpp.o
[ 29%] Building CXX object src/nlsat/CMakeFiles/nlsat.dir/nlsat_types.cpp.o
[ 29%] Built target rewriter
[ 29%] Generating "/Users/jamie/work/z3/build/x86/src/ast/normal_forms/nnf_params.hpp" from "nnf_params.pyg"
[ 29%] Building CXX object src/ast/rewriter/bit_blaster/CMakeFiles/bit_blaster.dir/bit_blaster.cpp.o
INFO:root:Using /Users/jamie/work/z3/src/ast/normal_forms/nnf_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/ast/normal_forms/nnf_params.hpp"
[ 29%] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/defined_names.cpp.o
[ 29%] Building CXX object src/ast/macros/CMakeFiles/macros.dir/macro_finder.cpp.o
[ 29%] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/elim_term_ite.cpp.o
[ 29%] Built target nlsat
[ 30%] Building CXX object src/ast/rewriter/bit_blaster/CMakeFiles/bit_blaster.dir/bit_blaster_rewriter.cpp.o
[ 30%] Building CXX object src/ast/macros/CMakeFiles/macros.dir/macro_manager.cpp.o
[ 30%] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/matcher.cpp.o
[ 30%] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/name_exprs.cpp.o
[ 30%] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/substitution.cpp.o
[ 30%] Building CXX object src/ast/macros/CMakeFiles/macros.dir/quantifier_macro_info.cpp.o
[ 30%] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/nnf.cpp.o
[ 30%] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/substitution_tree.cpp.o
[ 30%] Built target bit_blaster
[ 30%] Building CXX object src/ast/macros/CMakeFiles/macros.dir/macro_util.cpp.o
[ 30%] Building CXX object src/ast/macros/CMakeFiles/macros.dir/quasi_macros.cpp.o
[ 30%] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/pull_quant.cpp.o
[ 30%] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/unifier.cpp.o
[ 30%] Built target macros
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/binary_heap_priority_queue.cpp.o
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/binary_heap_upair_queue.cpp.o
[ 30%] Built target substitution
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/core_solver_pretty_printer.cpp.o
[ 30%] Building CXX object src/ast/proofs/CMakeFiles/proofs.dir/proof_checker.cpp.o
[ 30%] Building CXX object src/ast/proofs/CMakeFiles/proofs.dir/proof_utils.cpp.o
[ 30%] Built target normal_forms
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/dense_matrix.cpp.o
[ 30%] Generating "/Users/jamie/work/z3/build/x86/src/model/model_params.hpp" from "model_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/model/model_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/model/model_params.hpp"
[ 30%] Generating "/Users/jamie/work/z3/build/x86/src/model/model_evaluator_params.hpp" from "model_evaluator_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/model/model_evaluator_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/model/model_evaluator_params.hpp"
[ 30%] Building CXX object src/model/CMakeFiles/model.dir/array_factory.cpp.o
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/eta_matrix.cpp.o
[ 30%] Building CXX object src/model/CMakeFiles/model.dir/datatype_factory.cpp.o
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/emonics.cpp.o
[ 30%] Built target proofs
[ 30%] Building CXX object src/model/CMakeFiles/model.dir/func_interp.cpp.o
[ 30%] Building CXX object src/model/CMakeFiles/model.dir/model2expr.cpp.o
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/factorization.cpp.o
[ 30%] Building CXX object src/math/lp/CMakeFiles/lp.dir/factorization_factory_imp.cpp.o
[ 32%] Building CXX object src/model/CMakeFiles/model.dir/model_core.cpp.o
[ 32%] Building CXX object src/model/CMakeFiles/model.dir/model.cpp.o
[ 32%] Building CXX object src/model/CMakeFiles/model.dir/model_evaluator.cpp.o
[ 32%] Building CXX object src/math/lp/CMakeFiles/lp.dir/gomory.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/hnf_cutter.cpp.o
/Users/jamie/work/z3/src/model/model_evaluator.cpp:165:20: warning: unused variable 'g' [-Wunused-variable]
        func_decl* g = nullptr;
                   ^
1 warning generated.
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/horner.cpp.o
[ 33%] Building CXX object src/model/CMakeFiles/model.dir/model_implicant.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/indexed_vector.cpp.o
[ 33%] Building CXX object src/model/CMakeFiles/model.dir/model_macro_solver.cpp.o
[ 33%] Building CXX object src/model/CMakeFiles/model.dir/model_pp.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/int_branch.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/int_cube.cpp.o
[ 33%] Building CXX object src/model/CMakeFiles/model.dir/model_smt2_pp.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/int_gcd_test.cpp.o
[ 33%] Building CXX object src/model/CMakeFiles/model.dir/model_v2_pp.cpp.o
[ 33%] Building CXX object src/model/CMakeFiles/model.dir/numeral_factory.cpp.o
[ 33%] Building CXX object src/model/CMakeFiles/model.dir/struct_factory.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/int_solver.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lar_solver.cpp.o
[ 33%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lar_core_solver.cpp.o
[ 34%] Building CXX object src/model/CMakeFiles/model.dir/value_factory.cpp.o
[ 34%] Built target model
[ 34%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_core_solver_base.cpp.o
[ 34%] Generating "/Users/jamie/work/z3/build/x86/src/tactic/tactic_params.hpp" from "tactic_params.pyg"
INFO:root:Using /Users/jamie/work/z3/src/tactic/tactic_params.pyg
INFO:root:Generated "/Users/jamie/work/z3/build/x86/src/tactic/tactic_params.hpp"
[ 35%] Building CXX object src/tactic/CMakeFiles/tactic.dir/dependency_converter.cpp.o
[ 35%] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_arith.cpp.o
[ 35%] Building CXX object src/tactic/CMakeFiles/tactic.dir/equiv_proof_converter.cpp.o
[ 35%] Building CXX object src/tactic/CMakeFiles/tactic.dir/generic_model_converter.cpp.o
[ 35%] Building CXX object src/ast/fpa/CMakeFiles/fpa.dir/bv2fpa_converter.cpp.o
[ 35%] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_arrays.cpp.o
[ 35%] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal.cpp.o
[ 35%] Building CXX object src/ast/fpa/CMakeFiles/fpa.dir/fpa2bv_converter.cpp.o
[ 36%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_dual_core_solver.cpp.o
[ 36%] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal_num_occurs.cpp.o
[ 38%] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_datatypes.cpp.o
[ 38%] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal_shared_occs.cpp.o
[ 38%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_dual_simplex.cpp.o
[ 38%] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_plugin.cpp.o
[ 38%] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal_util.cpp.o
[ 38%] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_solve_plugin.cpp.o
[ 38%] Building CXX object src/tactic/CMakeFiles/tactic.dir/horn_subsume_model_converter.cpp.o
[ 38%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_primal_core_solver.cpp.o
[ 38%] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_term_graph.cpp.o
[ 38%] Building CXX object src/tactic/CMakeFiles/tactic.dir/model_converter.cpp.o
[ 38%] Building CXX object src/ast/fpa/CMakeFiles/fpa.dir/fpa2bv_rewriter.cpp.o
[ 39%] Building CXX object src/tactic/CMakeFiles/tactic.dir/probe.cpp.o
[ 39%] Built target fpa
[ 39%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_primal_simplex.cpp.o
[ 39%] Built target mbp
[ 39%] Building CXX object src/tactic/CMakeFiles/tactic.dir/proof_converter.cpp.o
[ 39%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_settings.cpp.o
[ 39%] Building CXX object src/tactic/CMakeFiles/tactic.dir/replace_proof_converter.cpp.o
[ 39%] Building CXX object src/smt/proto_model/CMakeFiles/proto_model.dir/proto_model.cpp.o
[ 39%] Building CXX object src/tactic/CMakeFiles/tactic.dir/tactical.cpp.o
[ 39%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_solver.cpp.o
[ 39%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lu.cpp.o
[ 39%] Built target proto_model
[ 39%] Building CXX object src/tactic/CMakeFiles/tactic.dir/tactic.cpp.o
[ 39%] Building CXX object src/math/lp/CMakeFiles/lp.dir/lp_utils.cpp.o
[ 39%] Built target tactic
[ 39%] Building CXX object src/sat/smt/CMakeFiles/sat_smt.dir/arith_axioms.cpp.o
[ 39%] Building CXX object src/sat/smt/CMakeFiles/sat_smt.dir/arith_diagnostics.cpp.o
[ 39%] Building CXX object src/sat/smt/CMakeFiles/sat_smt.dir/arith_internalize.cpp.o
In file included from /Users/jamie/work/z3/src/sat/smt/arith_axioms.cpp:18:
In file included from /Users/jamie/work/z3/src/sat/smt/euf_solver.h:30:
/Users/jamie/work/z3/src/sat/smt/user_solver.h:26:11: error: redefinition of 'user' as different kind of symbol
namespace user {
          ^
/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/user.h:87:8: note: previous definition is here
struct user {
       ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_axioms.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:104:9: error: no type named 'solver' in 'user'; did you mean simply 'solver'?
        user::solver*          m_user_propagator = nullptr;
        ^~~~~~~~~~~~
        solver
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:62:11: note: 'solver' declared here
    class solver : public sat::extension, public th_internalizer, public th_decompile {
          ^
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:253:46: error: no matching member function for call to 's'
        lbool value(enode* n) const { return s().value(enode2literal(n)); }
                                             ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'const euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'const euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_axioms.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:333:34: error: no matching member function for call to 's'
        bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
                                 ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_axioms.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:334:40: error: no matching member function for call to 's'
        sat::drat& get_drat() { return s().get_drat(); }
                                       ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
[ 39%] Building CXX object src/math/lp/CMakeFiles/lp.dir/matrix.cpp.o
In file included from /Users/jamie/work/z3/src/sat/smt/arith_diagnostics.cpp:18:
In file included from /Users/jamie/work/z3/src/sat/smt/euf_solver.h:30:
/Users/jamie/work/z3/src/sat/smt/user_solver.h:26:11: error: redefinition of 'user' as different kind of symbol
namespace user {
          ^
/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/user.h:87:8: note: previous definition is here
struct user {
       ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_internalize.cpp:18:
In file included from /Users/jamie/work/z3/src/sat/smt/euf_solver.h:30:
/Users/jamie/work/z3/src/sat/smt/user_solver.h:26:11: error: redefinition of 'user' as different kind of symbol
namespace user {
          ^
/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/user.h:87:8: note: previous definition is here
struct user {
       ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_diagnostics.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:104:9: error: no type named 'solver' in 'user'; did you mean simply 'solver'?
        user::solver*          m_user_propagator = nullptr;
        ^~~~~~~~~~~~
        solver
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:62:11: note: 'solver' declared here
    class solver : public sat::extension, public th_internalizer, public th_decompile {
          ^
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:253:46: error: no matching member function for call to 's'
        lbool value(enode* n) const { return s().value(enode2literal(n)); }
                                             ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'const euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'const euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_diagnostics.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:333:34: error: no matching member function for call to 's'
        bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
                                 ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_diagnostics.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:334:40: error: no matching member function for call to 's'
        sat::drat& get_drat() { return s().get_drat(); }
                                       ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_internalize.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:104:9: error: no type named 'solver' in 'user'; did you mean simply 'solver'?
        user::solver*          m_user_propagator = nullptr;
        ^~~~~~~~~~~~
        solver
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:62:11: note: 'solver' declared here
    class solver : public sat::extension, public th_internalizer, public th_decompile {
          ^
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:253:46: error: no matching member function for call to 's'
        lbool value(enode* n) const { return s().value(enode2literal(n)); }
                                             ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'const euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'const euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_internalize.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:333:34: error: no matching member function for call to 's'
        bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
                                 ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
In file included from /Users/jamie/work/z3/src/sat/smt/arith_internalize.cpp:18:
/Users/jamie/work/z3/src/sat/smt/euf_solver.h:334:40: error: no matching member function for call to 's'
        sat::drat& get_drat() { return s().get_drat(); }
                                       ^
/Users/jamie/work/z3/src/sat/sat_extension.h:75:17: note: candidate function not viable: no known conversion from 'euf::solver' to 'sat::extension' for object argument
        solver& s() { return *m_solver; }
                ^
/Users/jamie/work/z3/src/sat/sat_extension.h:76:23: note: candidate function not viable: no known conversion from 'euf::solver' to 'const sat::extension' for object argument
        solver const& s() const { return *m_solver; }
                      ^
[ 39%] Building CXX object src/math/lp/CMakeFiles/lp.dir/mon_eq.cpp.o
5 errors generated.
make[2]: *** [src/sat/smt/CMakeFiles/sat_smt.dir/arith_axioms.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/monomial_bounds.cpp.o
5 errors generated.
make[2]: *** [src/sat/smt/CMakeFiles/sat_smt.dir/arith_diagnostics.cpp.o] Error 1
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nex_creator.cpp.o
5 errors generated.
make[2]: *** [src/sat/smt/CMakeFiles/sat_smt.dir/arith_internalize.cpp.o] Error 1
make[1]: *** [src/sat/smt/CMakeFiles/sat_smt.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_basics_lemmas.cpp.o
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_common.cpp.o
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_core.cpp.o
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_intervals.cpp.o
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_monotone_lemmas.cpp.o
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_order_lemmas.cpp.o
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_solver.cpp.o
[ 40%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nla_tangent_lemmas.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/nra_solver.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/permutation_matrix.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/random_updater.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/row_eta_matrix.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/scaler.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/square_dense_submatrix.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/square_sparse_matrix.cpp.o
[ 41%] Building CXX object src/math/lp/CMakeFiles/lp.dir/static_matrix.cpp.o
[ 41%] Built target lp
make: *** [all] Error 2

I'm very rusty on C++ so was hoping someone might have some pointers - should I just be tweaking the CMAKE_CXX_FLAGS to change -Werror config, or is this something more problematic I'm missing?

@aytey
Copy link
Contributor

aytey commented Oct 9, 2021

Based on this:

/Users/jamie/work/z3/src/sat/smt/user_solver.h:26:11: error: redefinition of 'user' as different kind of symbol
namespace user {
          ^
/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/user.h:87:8: note: previous definition is here
struct user {

It seems that when you're building for this particular target, z3 ends-up #including sys/user.h , which declares a struct user -- this struct collides with z3's own "user" namespace. My guess is that something else in toolchain brings-in sys/user.h that doesn't happen "normally" (e.g., a regular x86 build).

At the top-level build folder (i.e., where you ran cmake), could you run something like:

make src/sat/smt/CMakeFiles/sat_smt.dir/arith_axioms.cpp.i
grep "^#" src/sat/smt/CMakeFiles/sat_smt.dir/arith_axioms.cpp.i | awk '{print $3}' | perl -ne 'print if ++$k{$_}==1'

This should (roughly) allow us to see what chain of includes leads to sys/user.h.

@jamiecollinson
Copy link
Contributor Author

Hi @andrewvaughanj, and thanks for taking a look. I get the following output:

"/Users/jamie/work/z3/src/sat/smt/arith_axioms.cpp"
"<built-in>"
"<command
"/Users/jamie/work/z3/src/sat/smt/euf_solver.h"
"/Users/jamie/work/z3/src/util/scoped_ptr_vector.h"
"/Users/jamie/work/z3/src/util/vector.h"
"/Users/jamie/work/z3/src/util/debug.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/stdlib.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__config"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/features.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/cdefs.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/android/versioning.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/android/api-level.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/get_device_api_level_inlines.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/android/ndk-version.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/local/include/stdlib.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/stdlib.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/alloca.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/wait.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/wait.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/malloc.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/stddef.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/lib64/clang/12.0.5/include/stddef.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/lib64/clang/12.0.5/include/__stddef_max_align_t.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__nullptr"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/stdio.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/stdio.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/stdint.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/lib64/clang/12.0.5/include/stdint.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/stdint.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/wchar_limits.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/int-ll64.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/bitsperlong.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/bitsperlong.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/posix_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/stddef.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/compiler_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/compiler.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/posix_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/posix_types_32.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/posix_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/pthread_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/lib64/clang/12.0.5/include/stdarg.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/seek_constants.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/struct_file.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/xlocale.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/android/legacy_stdlib_inlines.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/math.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/local/include/math.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/math.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/limits.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/lib64/clang/12.0.5/include/limits.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/limits.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/float.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/lib64/clang/12.0.5/include/float.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/limits.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/posix_limits.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/type_traits"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cstddef"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/version"
diagnostic
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/limits"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__undef_macros"
"/Users/jamie/work/z3/src/util/error_codes.h"
"/Users/jamie/work/z3/src/util/warning.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/iostream"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/ios"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/iosfwd"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/wchar.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/local/include/wchar.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/wchar.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/time.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/time.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/time.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/time_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/select.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/signal.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/sigcontext.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/signal_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/signal.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/signal.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/signal-defs.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/siginfo.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/siginfo.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/timespec.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/ucontext.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/user.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/android/legacy_signal_inlines.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/mbstate_t.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/wctype.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__locale"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/string"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/string_view"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__string"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/algorithm"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/initializer_list"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cstring"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/string.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/string.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/strcasecmp.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/strings.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/utility"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__tuple"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cstdint"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__debug"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/memory"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/typeinfo"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/exception"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cstdlib"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/new"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/iterator"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__functional_base"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/tuple"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/stdexcept"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/atomic"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__threading_support"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/chrono"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/ctime"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/ratio"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/climits"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/errno.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/errno.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/errno.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/i686-linux-android/asm/errno.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/errno.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/asm-generic/errno-base.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/android/legacy_errno_inlines.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/pthread.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sched.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/linux/sched.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/semaphore.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/functional"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/bit"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cstdio"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cwchar"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cwctype"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cctype"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/ctype.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/ctype.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/bits/ctype_inlines.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/wctype.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/local/include/wctype.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/wctype.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/mutex"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__mutex_base"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/system_error"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__errc"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cerrno"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/locale.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/local/include/locale.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/locale.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/support/android/locale_bionic.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/streambuf"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/istream"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/ostream"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/locale"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cstdarg"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__bsd_locale_fallbacks.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/bitset"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__bit_reference"
"/Users/jamie/work/z3/src/util/memory_manager.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/iomanip"
"/Users/jamie/work/z3/src/util/z3_exception.h"
"/Users/jamie/work/z3/src/util/hash.h"
"/Users/jamie/work/z3/src/util/util.h"
"/Users/jamie/work/z3/src/util/trail.h"
"/Users/jamie/work/z3/src/util/obj_hashtable.h"
"/Users/jamie/work/z3/src/util/hashtable.h"
"/Users/jamie/work/z3/src/util/region.h"
"/Users/jamie/work/z3/src/util/obj_ref.h"
"/Users/jamie/work/z3/src/ast/ast_translation.h"
"/Users/jamie/work/z3/src/ast/ast.h"
"/Users/jamie/work/z3/src/util/buffer.h"
"/Users/jamie/work/z3/src/util/zstring.h"
"/Users/jamie/work/z3/src/util/rational.h"
"/Users/jamie/work/z3/src/util/mpq.h"
"/Users/jamie/work/z3/src/util/mpz.h"
"/Users/jamie/work/z3/src/util/mutex.h"
"/Users/jamie/work/z3/src/util/small_object_allocator.h"
"/Users/jamie/work/z3/src/util/machine.h"
"/Users/jamie/work/z3/src/util/trace.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/fstream"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/filesystem"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/stack"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/deque"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__split_buffer"
"/Users/jamie/work/z3/src/util/scoped_numeral.h"
"/Users/jamie/work/z3/src/util/scoped_numeral_vector.h"
"/Users/jamie/work/z3/src/util/mpn.h"
"/Users/jamie/work/z3/src/util/symbol.h"
"/Users/jamie/work/z3/src/util/tptr.h"
"/Users/jamie/work/z3/src/util/string_buffer.h"
"/Users/jamie/work/z3/src/util/optional.h"
"/Users/jamie/work/z3/src/util/bit_vector.h"
"/Users/jamie/work/z3/src/util/symbol_table.h"
"/Users/jamie/work/z3/src/util/ref_vector.h"
"/Users/jamie/work/z3/src/util/ref.h"
"/Users/jamie/work/z3/src/util/ref_pair_vector.h"
"/Users/jamie/work/z3/src/util/ref_buffer.h"
"/Users/jamie/work/z3/src/util/obj_mark.h"
"/Users/jamie/work/z3/src/util/id_gen.h"
"/Users/jamie/work/z3/src/util/map.h"
"/Users/jamie/work/z3/src/util/parray.h"
"/Users/jamie/work/z3/src/util/dictionary.h"
"/Users/jamie/work/z3/src/util/chashtable.h"
"/Users/jamie/work/z3/src/util/dependency.h"
"/Users/jamie/work/z3/src/util/rlimit.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/variant"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/array"
"/Users/jamie/work/z3/src/ast/euf/euf_egraph.h"
"/Users/jamie/work/z3/src/util/statistics.h"
"/Users/jamie/work/z3/src/util/lbool.h"
"/Users/jamie/work/z3/src/ast/euf/euf_enode.h"
"/Users/jamie/work/z3/src/util/id_var_list.h"
"/Users/jamie/work/z3/src/util/approx_set.h"
"/Users/jamie/work/z3/src/util/sat_literal.h"
"/Users/jamie/work/z3/src/util/uint_set.h"
"/Users/jamie/work/z3/src/ast/euf/euf_justification.h"
"/Users/jamie/work/z3/src/ast/euf/euf_etable.h"
"/Users/jamie/work/z3/src/ast/ast_ll_pp.h"
"/Users/jamie/work/z3/src/ast/rewriter/th_rewriter.h"
"/Users/jamie/work/z3/src/ast/rewriter/rewriter_types.h"
"/Users/jamie/work/z3/src/util/common_msgs.h"
"/Users/jamie/work/z3/src/util/params.h"
"/Users/jamie/work/z3/src/util/cmd_context_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/sstream"
"/Users/jamie/work/z3/src/tactic/model_converter.h"
"/Users/jamie/work/z3/src/ast/ast_pp_util.h"
"/Users/jamie/work/z3/src/ast/decl_collector.h"
"/Users/jamie/work/z3/src/util/top_sort.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/memory.h"
"/Users/jamie/work/z3/src/ast/datatype_decl_plugin.h"
"/Users/jamie/work/z3/src/ast/ast_smt2_pp.h"
"/Users/jamie/work/z3/src/ast/format.h"
"/Users/jamie/work/z3/src/ast/arith_decl_plugin.h"
"/Users/jamie/work/z3/src/ast/bv_decl_plugin.h"
"/Users/jamie/work/z3/src/ast/array_decl_plugin.h"
"/Users/jamie/work/z3/src/ast/fpa_decl_plugin.h"
"/Users/jamie/work/z3/src/util/mpf.h"
"/Users/jamie/work/z3/src/ast/dl_decl_plugin.h"
"/Users/jamie/work/z3/src/ast/seq_decl_plugin.h"
"/Users/jamie/work/z3/src/ast/char_decl_plugin.h"
"/Users/jamie/work/z3/src/ast/ast_smt_pp.h"
"/Users/jamie/work/z3/src/util/smt2_util.h"
"/Users/jamie/work/z3/src/model/model.h"
"/Users/jamie/work/z3/src/util/plugin_manager.h"
"/Users/jamie/work/z3/src/model/model_core.h"
"/Users/jamie/work/z3/src/model/func_interp.h"
"/Users/jamie/work/z3/src/model/model_evaluator.h"
"/Users/jamie/work/z3/src/model/value_factory.h"
"/Users/jamie/work/z3/src/tactic/converter.h"
"/Users/jamie/work/z3/src/sat/sat_extension.h"
"/Users/jamie/work/z3/src/sat/sat_types.h"
"/Users/jamie/work/z3/src/util/stopwatch.h"
"/Users/jamie/work/z3/src/sat/smt/atom2bool_var.h"
"/Users/jamie/work/z3/src/ast/expr2var.h"
"/Users/jamie/work/z3/src/sat/smt/sat_th.h"
"/Users/jamie/work/z3/src/sat/smt/sat_smt.h"
"/Users/jamie/work/z3/src/ast/ast_pp.h"
"/Users/jamie/work/z3/src/sat/sat_solver.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/cmath"
"/Users/jamie/work/z3/src/util/var_queue.h"
"/Users/jamie/work/z3/src/util/heap.h"
"/Users/jamie/work/z3/src/util/ema.h"
"/Users/jamie/work/z3/src/util/scoped_limit_trail.h"
"/Users/jamie/work/z3/src/sat/sat_clause.h"
"/Users/jamie/work/z3/src/sat/sat_allocator.h"
"/Users/jamie/work/z3/src/sat/sat_watched.h"
"/Users/jamie/work/z3/src/sat/sat_justification.h"
"/Users/jamie/work/z3/src/sat/sat_config.h"
"/Users/jamie/work/z3/src/sat/sat_cleaner.h"
"/Users/jamie/work/z3/src/sat/sat_simplifier.h"
"/Users/jamie/work/z3/src/sat/sat_clause_set.h"
"/Users/jamie/work/z3/src/sat/sat_clause_use_list.h"
"/Users/jamie/work/z3/src/sat/sat_model_converter.h"
"/Users/jamie/work/z3/src/sat/sat_scc.h"
"/Users/jamie/work/z3/src/sat/sat_big.h"
"/Users/jamie/work/z3/src/sat/sat_asymm_branch.h"
"/Users/jamie/work/z3/src/sat/sat_cut_simplifier.h"
"/Users/jamie/work/z3/src/util/union_find.h"
"/Users/jamie/work/z3/src/sat/sat_aig_finder.h"
"/Users/jamie/work/z3/src/sat/sat_aig_cuts.h"
"/Users/jamie/work/z3/src/sat/sat_cutset.h"
"/Users/jamie/work/z3/src/sat/sat_probing.h"
"/Users/jamie/work/z3/src/sat/sat_mus.h"
"/Users/jamie/work/z3/src/sat/sat_binspr.h"
"/Users/jamie/work/z3/src/sat/sat_drat.h"
"/Users/jamie/work/z3/src/sat/sat_parallel.h"
"/Users/jamie/work/z3/src/sat/sat_local_search.h"
"/Users/jamie/work/z3/src/sat/sat_solver_core.h"
"/Users/jamie/work/z3/src/sat/smt/sat_internalizer.h"
"/Users/jamie/work/z3/src/smt/params/smt_params.h"
"/Users/jamie/work/z3/src/smt/params/dyn_ack_params.h"
"/Users/jamie/work/z3/src/smt/params/qi_params.h"
"/Users/jamie/work/z3/src/smt/params/theory_arith_params.h"
"/Users/jamie/work/z3/src/smt/params/theory_array_params.h"
"/Users/jamie/work/z3/src/smt/params/theory_bv_params.h"
"/Users/jamie/work/z3/src/smt/params/theory_str_params.h"
"/Users/jamie/work/z3/src/smt/params/theory_seq_params.h"
"/Users/jamie/work/z3/src/smt/params/theory_pb_params.h"
"/Users/jamie/work/z3/src/smt/params/theory_datatype_params.h"
"/Users/jamie/work/z3/build/x86/src/smt/params/smt_params_helper.hpp"
"/Users/jamie/work/z3/src/util/gparams.h"
"/Users/jamie/work/z3/src/smt/params/preprocessor_params.h"
"/Users/jamie/work/z3/src/params/pattern_inference_params.h"
"/Users/jamie/work/z3/src/params/bit_blaster_params.h"
"/Users/jamie/work/z3/src/params/context_params.h"
"/Users/jamie/work/z3/src/sat/smt/sat_dual_solver.h"
"/Users/jamie/work/z3/src/util/lim_vector.h"
"/Users/jamie/work/z3/src/sat/smt/euf_ackerman.h"
"/Users/jamie/work/z3/src/util/dlist.h"
"/Users/jamie/work/z3/src/sat/smt/user_solver.h"
"/Users/jamie/work/z3/src/solver/solver.h"
"/Users/jamie/work/z3/src/solver/check_sat_result.h"
"/Users/jamie/work/z3/src/util/event_handler.h"
"/Users/jamie/work/z3/src/util/timer.h"
"/Users/jamie/work/z3/src/solver/progress_callback.h"
"/Users/jamie/work/z3/src/sat/smt/arith_solver.h"
"/Users/jamie/work/z3/src/util/obj_pair_set.h"
"/Users/jamie/work/z3/src/ast/ast_trail.h"
"/Users/jamie/work/z3/src/math/lp/lp_solver.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/unordered_map"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__hash_table"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__node_handle"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/optional"
"/Users/jamie/work/z3/src/math/lp/lp_settings.h"
"/Users/jamie/work/z3/src/math/lp/lp_utils.h"
"/Users/jamie/work/z3/src/math/lp/numeric_pair.h"
"/Users/jamie/work/z3/src/util/sstream.h"
"/Users/jamie/work/z3/src/math/lp/lp_types.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/unordered_set"
"/Users/jamie/work/z3/src/math/lp/column_info.h"
"/Users/jamie/work/z3/src/math/lp/static_matrix.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/set"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/__tree"
"/Users/jamie/work/z3/src/math/lp/sparse_vector.h"
"/Users/jamie/work/z3/src/math/lp/indexed_vector.h"
"/Users/jamie/work/z3/src/math/lp/permutation_matrix.h"
"/Users/jamie/work/z3/src/math/lp/matrix.h"
"/Users/jamie/work/z3/src/math/lp/tail_matrix.h"
"/Users/jamie/work/z3/src/math/lp/lp_core_solver_base.h"
"/Users/jamie/work/z3/src/math/lp/core_solver_pretty_printer.h"
"/Users/jamie/work/z3/src/math/lp/lu.h"
"/Users/jamie/work/z3/src/math/lp/square_sparse_matrix.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/queue"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/vector"
"/Users/jamie/work/z3/src/math/lp/indexed_value.h"
"/Users/jamie/work/z3/src/math/lp/eta_matrix.h"
"/Users/jamie/work/z3/src/math/lp/binary_heap_upair_queue.h"
"/Users/jamie/work/z3/src/math/lp/binary_heap_priority_queue.h"
"/Users/jamie/work/z3/src/math/lp/u_set.h"
"/Users/jamie/work/z3/src/math/lp/row_eta_matrix.h"
"/Users/jamie/work/z3/src/math/lp/square_dense_submatrix.h"
"/Users/jamie/work/z3/src/math/lp/dense_matrix.h"
"/Users/jamie/work/z3/src/math/lp/column_namer.h"
"/Users/jamie/work/z3/src/math/lp/scaler.h"
"/Users/jamie/work/z3/src/math/lp/bound_analyzer_on_row.h"
"/Users/jamie/work/z3/src/math/lp/implied_bound.h"
"/Users/jamie/work/z3/src/math/lp/lar_constraints.h"
"/Users/jamie/work/z3/src/util/stacked_value.h"
"/Users/jamie/work/z3/src/math/lp/ul_pair.h"
"/Users/jamie/work/z3/src/math/lp/lar_term.h"
"/Users/jamie/work/z3/src/math/lp/test_bound_analyzer.h"
"/Users/jamie/work/z3/src/math/lp/lp_primal_simplex.h"
"/Users/jamie/work/z3/src/math/lp/lp_primal_core_solver.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/list"
"/Users/jamie/work/z3/src/math/lp/breakpoint.h"
"/Users/jamie/work/z3/src/math/lp/lp_dual_simplex.h"
"/Users/jamie/work/z3/src/math/lp/lp_dual_core_solver.h"
"/Users/jamie/work/z3/src/math/lp/lar_solver.h"
"/Users/jamie/work/z3/src/math/lp/lar_core_solver.h"
"/Users/jamie/work/z3/src/math/lp/stacked_vector.h"
"/Users/jamie/work/z3/src/math/lp/lar_solution_signature.h"
"/Users/jamie/work/z3/src/math/lp/random_updater.h"
"/Users/jamie/work/z3/src/math/lp/conversion_helper.h"
"/Users/jamie/work/z3/src/math/lp/int_solver.h"
"/Users/jamie/work/z3/src/math/lp/hnf_cutter.h"
"/Users/jamie/work/z3/src/math/lp/hnf.h"
"/Users/jamie/work/z3/src/util/ext_gcd.h"
"/Users/jamie/work/z3/src/math/lp/general_matrix.h"
"/Users/jamie/work/z3/src/math/lp/var_register.h"
"/Users/jamie/work/z3/src/math/lp/lia_move.h"
"/Users/jamie/work/z3/src/math/lp/explanation.h"
"/Users/jamie/work/z3/src/math/lp/int_gcd_test.h"
"/Users/jamie/work/z3/src/math/lp/nra_solver.h"
"/Users/jamie/work/z3/src/nlsat/nlsat_solver.h"
"/Users/jamie/work/z3/src/nlsat/nlsat_types.h"
"/Users/jamie/work/z3/src/math/polynomial/polynomial.h"
"/Users/jamie/work/z3/src/util/mpbqi.h"
"/Users/jamie/work/z3/src/util/mpbq.h"
"/Users/jamie/work/z3/src/util/basic_interval.h"
"/Users/jamie/work/z3/src/util/sign.h"
"/Users/jamie/work/z3/src/math/lp/lp_bound_propagator.h"
"/Users/jamie/work/z3/src/math/lp/nla_solver.h"
"/Users/jamie/work/z3/src/math/lp/monic.h"
"/Users/jamie/work/z3/src/math/lp/nla_defs.h"
"/Users/jamie/work/z3/src/math/lp/nla_settings.h"
"/Users/jamie/work/z3/src/math/lp/nla_core.h"
"/Users/jamie/work/z3/src/math/lp/factorization.h"
"/Users/jamie/work/z3/src/math/lp/var_eqs.h"
"/Users/jamie/work/z3/src/math/lp/incremental_vector.h"
"/Users/jamie/work/z3/src/math/lp/nla_tangent_lemmas.h"
"/Users/jamie/work/z3/src/math/lp/nla_common.h"
"/Users/jamie/work/z3/src/math/lp/emonics.h"
"/Users/jamie/work/z3/src/math/lp/nex_creator.h"
"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/c++/v1/map"
"/Users/jamie/work/z3/src/math/lp/nex.h"
"/Users/jamie/work/z3/src/math/lp/nla_basics_lemmas.h"
"/Users/jamie/work/z3/src/math/lp/nla_order_lemmas.h"
"/Users/jamie/work/z3/src/math/lp/nla_monotone_lemmas.h"
"/Users/jamie/work/z3/src/math/lp/horner.h"
"/Users/jamie/work/z3/src/math/lp/nla_intervals.h"
"/Users/jamie/work/z3/src/math/interval/interval.h"
"/Users/jamie/work/z3/src/util/ext_numeral.h"
"/Users/jamie/work/z3/src/math/interval/dep_intervals.h"
"/Users/jamie/work/z3/src/math/lp/cross_nested.h"
"/Users/jamie/work/z3/src/math/lp/monomial_bounds.h"
"/Users/jamie/work/z3/src/math/grobner/pdd_solver.h"
"/Users/jamie/work/z3/src/math/dd/dd_pdd.h"
"/Users/jamie/work/z3/src/math/lp/lp_api.h"
"/Users/jamie/work/z3/src/util/inf_rational.h"
"/Users/jamie/work/z3/src/math/polynomial/algebraic_numbers.h"

Which grepping for user shows:

"/Users/jamie/Library/Android/sdk/ndk/23.0.7599858/toolchains/llvm/prebuilt/darwin-x86_64/bin/../sysroot/usr/include/sys/user.h"
"/Users/jamie/work/z3/src/sat/smt/user_solver.h"

So I'd guess your hunch is right re: user.h, and hopefully all the other errors cascade from that.

Any pointers on what I can do to investigate further / fix? I'm definitely out of my depth here so all help appreciated :-)

aytey added a commit to aytey/z3 that referenced this issue Oct 9, 2021
Issue Z3Prover#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 <[email protected]>

Signed-off-by: Andrew V. Jones <[email protected]>
aytey added a commit to aytey/z3 that referenced this issue Oct 9, 2021
Issue Z3Prover#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 <[email protected]>

Signed-off-by: Andrew V. Jones <[email protected]>
@aytey
Copy link
Contributor

aytey commented Oct 9, 2021

So, a brief look at this suggests that signal.h (in android-ndk-r23) brings in ucontext.h (which then brings-in its sys version), which brings in sys/user.h. If you go higher-up, iostream under (e.g.,) i686-linux-android30-clang++ brings in sys/user.h (via signal.h).

I opened #5587 to try and fix this for you.

aytey added a commit to aytey/z3 that referenced this issue Oct 9, 2021
Issue Z3Prover#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 <[email protected]>

Signed-off-by: Andrew V. Jones <[email protected]>
NikolajBjorner pushed a commit that referenced this issue Oct 9, 2021
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 <[email protected]>

Signed-off-by: Andrew V. Jones <[email protected]>
@jamiecollinson
Copy link
Contributor Author

jamiecollinson commented Oct 10, 2021

Worked perfectly, and I've built all my desired targets (arm64-v8a, armeabi-v7a, x86 and x86_64) with android-ndk-r23 so fairly confident that'll resolve it for anyone looking to build for other targets too.

Thanks - assistance much appreciated and if there's anything else Android related I can do to help the project let me know.

@NikolajBjorner
Copy link
Contributor

For catching any regressions at build time you are invited to add pipeline definitions to either our GitHub Actions or CI/Nightly Azure pipelines.

@jamiecollinson
Copy link
Contributor Author

@NikolajBjorner I was thinking about doing that, as it wouldn't be a big step from the build script I've created (linked in first post). What would be best, I'm guessing Azure pipelines since that's where the other binary builds are happening?

@NikolajBjorner
Copy link
Contributor

I just looked at the script. It looks like it is mainly about ensuring that the VM has pulls the right SDK (apt-get).

Azure pipelines have more features but are heavier to dance with. Github action are more modular and can be run on every build. How about creating a github action and I can take it from there?

@NikolajBjorner
Copy link
Contributor

NikolajBjorner commented Oct 10, 2021

It is something like


name: Android Build

on:
  push:
    branches: [ master ]

env:
  BUILD_TYPE: Release

jobs:
  build:
    runs-on: ubuntu-latest

    steps:
    - uses: actions/checkout@v2

    - name: Configure CMake
      run:    cmake -DCMAKE_BUILD_TYPE= ${{env.BUILD_TYPE}} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_SYSTEM_VERSION=21 -DCMAKE_ANDROID_ARCH_ABI=$androidABI -DCMAKE_ANDROID_NDK=$NDK -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" -DJAVA_AWT_LIBRARY=NotNeeded -DJAVA_JVM_LIBRARY=NotNeeded -DJAVA_INCLUDE_PATH2=NotNeeded -DJAVA_AWT_INCLUDE_PATH=NotNeeded ../../
 

    - name: Build
      # Build your program with the given configuration
      run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}}

    - name: Clone z3test
      run: git clone https://github.com/z3prover/z3test z3test
    
    - name: Run regressions
      run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2   

where you have to replace $androidAPI with something like with ${{ }} and set up a matrix (not in this script, but it seems to be

      matrix:
        target: [arm64-v8a, armeabi-v7a, x86, x86_64t]

Of course it takes up some time to write and test this script.

@jamiecollinson
Copy link
Contributor Author

Leave it with me and I'll take a look. I know Azure pipelines have an instance with NDK already installed (not sure if Github actions do) but I'll start with GitHub actions as I've more experience with them.

saruman9 added a commit to saruman9/LibAFL that referenced this issue Jul 19, 2023
See Z3Prover/z3#5586. libafl with `cmin` feature cannot be builded for Android.
saruman9 added a commit to saruman9/LibAFL that referenced this issue Jul 24, 2023
See Z3Prover/z3#5586. libafl with `cmin` feature cannot be built for Android.
domenukk pushed a commit to AFLplusplus/LibAFL that referenced this issue Jul 24, 2023
See Z3Prover/z3#5586. libafl with `cmin` feature cannot be built for Android.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants