Add commands:
(prefer <formula>)
- will instruct case split queue to assign formula to true.
- prefer commands added within a scope are forgotten after leaving the scope.
(reset-preferences)
- resets asserted preferences. Has to be invoked at base level.
This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2
* Add comprehensive API special relations tests
- Implement tests for all 5 special relations API functions:
* Z3_mk_linear_order - Linear order relation
* Z3_mk_partial_order - Partial order relation
* Z3_mk_piecewise_linear_order - Piecewise linear order relation
* Z3_mk_tree_order - Tree order relation
* Z3_mk_transitive_closure - Transitive closure of a relation
- Test coverage achieved: 100% (5/5 lines) in src/api/api_special_relations.cpp
- Added comprehensive test cases covering:
* Basic functionality with different sorts
* Different index parameters
* Expression creation and integration
* Edge cases and variations
🤖 Generated with Claude Code
* staged files
* remove files
---------
Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
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>
