On macOS, libz3java.dylib was built without an rpath to find
libz3.dylib in the same directory. When Java loaded the JNI library,
the dynamic linker could not resolve the libz3 dependency, causing
UnsatisfiedLinkError.
Three fixes:
- mk_util.py: add -Wl,-rpath,@loader_path to the macOS JNI link command
- CMakeLists.txt: set MACOSX_RPATH, BUILD_RPATH, INSTALL_RPATH for
z3java target; remove duplicate headerpad block
- update_api.py: improve Native.java error message to show the root
cause from both load attempts instead of only the fallback error
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When macos-latest changed to ARM64 runners, the mac-build-x64 job started
producing arm64 libz3.dylib inside x86_64-tagged wheels, causing import
failures on macOS x86_64.
Root cause: mk_make.py subprocess detects the ARM64 host at module level
(IS_ARCH_ARM64=True), and without --arm64=false override it adds -arch arm64
to SLIBEXTRAFLAGS, overriding the -arch x86_64 set via environment variables.
Fix 1 (mk_unix_dist.py): Pass --arm64=false to mk_make.py subprocess when
building x64 on an ARM64 host, preventing the arm64 flag inheritance.
Fix 2 (mk_util.py): When IS_ARCH_ARM64=False on an ARM64 macOS host, add
-arch x86_64 to SLIBEXTRAFLAGS so the shared library linker also targets
x86_64 (LDFLAGS already receives this flag from the env var).
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
The addition of -fomit-frame-pointer was missing a space (which broke
the command line), but also this option should be added only if -pg is
*not* given, as they are incompatible. So, just remove this line to fix
the --gprof flag in configure.
Also, this option is implied by any level of `-O`, so there is no need
to pass it explicitly in most cases. It could be added to debug,
non-profile builds, but I'm not sure that's useful.
* Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it.
* Fix configuration error for non-MSVC compilers.
* Reviewed and updated configuration for Python build and added comment for CFG.
* WiP: test build specific version number
* update mk_win_dist for assembly-version
* Add print statements for version
* remove stray semicolon
* undo quote change in projectstr
* nit fixes
* revert print formatting for Mac build
* fix spaces
* WiP: publish symbols for package
* set debugtype to full
* fix internal nuget feed publishing
* Try pipeline github authorization
* Update github service connection
* WiP: try symbol publish in build
* try Z3Prover for GitHub connection
* WiP: collect symbols
* revert symbol type to pdbonly (only portable is not supported for publishing)
* Publish symbols in nightly and release
* Revert this: comment out publish to test release build pipe
* restore publishing
* Turn of index sources to eliminate warning that it is not supported for Github
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
These are all unused and shouldn't be needed. Mostly we need
something for differentiating between POSIX and non-POSIX
(until we can reduce some of those differences as well).
We shouldn't need to modify the build system to build on a new
OS if it is basically a Unix and is supported by cmake.
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)
`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
Make it easier to add native methods for callbacks (for user propagator) #6097
The Java User propagator wrapper should define a base class with virtual methods that can be invoked from functions defined in NativeStatic.txt
* [Draft] Added unfinished code for high level bindings for js
* * Rewrote structure of js api files
* Added more high level apis
* Minor fixes
* Fixed wasm github action
* Fix JS test
* Removed ContextOptions type
* * Added Ints to JS Api
* Added tests to JS Api
* Added run-time checks for contexts
* Removed default contexts
* Merged Context and createContext so that the api behaves the sames as in other constructors
* Added a test for Solver
* Added Reals
* Added classes for IntVals and RealVals
* Added abillity to specify logic for solver
* Try to make CI tests not fail
* Changed APIs after a round of review
* Fix test
* Added BitVectors
* Made sort into getter
* Added initial JS docs
* Added more coercible types
* Removed done TODOs
* Dispose of intermediate Z3Objects created in dotnet api.
* Set C# LangVersion to 8.0.
* Fix build errors.
* Fix warning about empty using statement.
* Fix Xor to only dispose of objects that it creates internally.
