Z3Prover / z3

The Z3 Theorem Prover
Other
10.35k stars 1.48k forks source link

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

Closed jamiecollinson closed 3 years ago

jamiecollinson commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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.

jamiecollinson commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

@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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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.