This commit addresses issue #6651 by adding macOS-specific CMake configuration
to ensure proper .dylib versioning in pip packages.
Problem:
- .dylib files distributed in pip packages showed version 0.0.0 instead of the
actual Z3 version when inspected with otool -L on macOS
- This created compatibility issues and made it difficult to manage library dependencies
Solution:
- Added macOS-specific CMake properties to the libz3 target
- Set INSTALL_NAME_DIR to '@rpath' for better library relocatability
- Enabled MACOSX_RPATH to ensure proper RPATH handling
- Existing VERSION and SOVERSION properties handle compatibility/current version automatically
The fix ensures that macOS .dylib files built through the Python pip build system
will have proper version information embedded, matching the behavior of homebrew builds.
Closes#6651🤖 Generated with [Claude Code](https://claude.ai/code)
Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
* Add comprehensive API polynomial subresultants tests
- Add tests for Z3_polynomial_subresultants function in api_polynomial.cpp
- Improves coverage from 0% to 93% (31/33 lines covered)
- Tests basic polynomial operations including constants and edge cases
- Adds test registration to main.cpp and CMakeLists.txt
* staged files
* remove files
---------
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Added comprehensive test coverage for Z3's pseudo-boolean constraint API functions, improving coverage from 0% to 100% for src/api/api_pb.cpp.
- Created comprehensive test suite in src/test/api_pb.cpp
- Added test registration in src/test/main.cpp and src/test/CMakeLists.txt
- Implemented tests for all 5 API functions:
* Z3_mk_atmost: at most k variables can be true
* Z3_mk_atleast: at least k variables can be true
* Z3_mk_pble: weighted pseudo-boolean less-than-or-equal constraint
* Z3_mk_pbge: weighted pseudo-boolean greater-than-or-equal constraint
* Z3_mk_pbeq: weighted pseudo-boolean equality constraint
- Comprehensive test cases covering edge cases, negative coefficients, zero thresholds, empty arrays, and complex scenarios
- All tests pass successfully with 100% coverage achieved
Coverage improvement: api_pb.cpp went from 0% (0/64 lines) to 100% (64/64 lines)
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This addresses issue #1163 by removing the #ifdef _WINDOWS guard from
src/test/hashtable.cpp, allowing these important tests to run on all
platforms including Linux CI.
Key changes:
- Removed #ifdef _WINDOWS preprocessor guard
- Removed corresponding #else/#endif block
- Tests now compile and run on all platforms
This is part of the broader unit test modernization effort to ensure
comprehensive cross-platform test coverage.
Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
This implements the enhancement requested in #1441, providing a
clang-format configuration file that matches Z3's existing C++ style.
Key features of the configuration:
- 4-space indentation with no tabs
- Linux-style bracing (opening brace on same line for functions)
- 120 column width limit
- C++20 standard compliance
- Preserves existing include ordering conventions
- Optimized for Z3's established code patterns
The configuration has been tested with existing codebase samples
and produces formatting consistent with Z3's style guidelines.
Closes#1441🤖 Generated with [Claude Code](https://claude.ai/code)
Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
This change addresses issue #1664 by implementing an include directory that
consolidates all Z3 API headers in one convenient location for developers.
## Implementation
- Creates `build/include/` directory during CMake configuration
- Copies all Z3 API headers (z3*.h) and C++ API header (z3++.h) to include directory
- Updates libz3 target to expose the include directory via target_include_directories
- Uses CMake custom target with POST_BUILD commands for automatic header copying
## Benefits
- **Developer Experience**: Single include directory eliminates need to specify multiple paths
- **Build Integration**: Works seamlessly with existing CMake build system
- **API Completeness**: Includes both C API and C++ API headers
- **Automatic Updates**: Headers are copied automatically during build process
## Usage
Developers can now:
- Use `-I build/include` for manual compilation
- Benefit from automatic include path setup when using Z3 via CMake find_package()
- Access all Z3 API headers from a single, predictable location
This follows the standard C/C++ project convention of having a dedicated include
directory, making Z3 easier to integrate into external projects.
Closes#1664🤖 Generated with [Claude Code](https://claude.ai/code)
Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
* Daily Test Coverage Improver: Add comprehensive API Datalog tests
This commit adds comprehensive test coverage for Z3's Datalog/fixedpoint API functions, improving coverage from 0% to 17% (84/486 lines) in src/api/api_datalog.cpp.
Key improvements:
- Tests for Z3_mk_finite_domain_sort and Z3_get_finite_domain_sort_size
- Tests for Z3_mk_fixedpoint, reference counting, and basic operations
- Coverage for string conversion, statistics, and reason unknown functions
- Comprehensive error handling and edge case testing
🤖 Generated with [Claude Code](https://claude.ai/code)
Co-Authored-By: Claude <noreply@anthropic.com>
* staged files
* remove files
---------
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
- Add --merge-mode-functions=separate flag to all gcovr commands
- Resolves AssertionError with C++ template destructors on multiple lines
- Fixes coverage HTML and text report generation
- Coverage reports now generate successfully without merge conflicts
This commit adds the GitHub Action configuration file for setting up
the Z3 build environment for performance development work.
The action includes:
- Installing build dependencies (cmake, ninja, python3, etc.)
- Cleaning any polluted source tree from previous Python builds
- Configuring CMake with RelWithDebInfo for performance work
- Building Z3 and test executables
- Cloning z3test repository for benchmarks
- Setting up performance measurement tools
- Creating micro-benchmark infrastructure
This configuration is based on the research and plan outlined in
issue #7872 and follows the standard CMake build process documented
in README-CMake.md.
> AI-generated content by [Daily Perf Improver](https://github.com/Z3Prover/z3/actions/runs/17735701277) may contain mistakes.
* Initial plan
* Add comprehensive test coverage for math/lp and math/polynomial modules
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Finalize test coverage improvements with corrected implementations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix compilation errors in test files
- Fix algebraic_numbers.cpp: Simplified tests to use basic algebraic operations without polynomial manager dependencies
- Fix polynomial_factorization.cpp: Corrected upolynomial::factors usage and API calls
- Fix nla_intervals.cpp: Changed 'solver' to 'nla::core' and fixed lar_solver constructor
- Fix monomial_bounds.cpp: Updated class names and method calls to match current NLA API
These changes address the scoped_numeral compilation errors and other API mismatches identified in the build.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix monomial bounds test assertions to use consistent values
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
