mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity
20751 commits 65 branches 58 tags 180 MiB
Commit graph

17289 commits

Author SHA1 Message Date
Nikolaj Bjorner
487db1a658 Modify behavior for division by zero 
Allow division by zero in z3 expressions without raising an error.
 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
bcc87975e5 Delete src/api/python/test_critical_fixes.py 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
25c2b7e4c1 Fix error message capitalization for Python conventions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
0ee04d25c8 Add comprehensive tests for Python API bug fixes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
28db5e2440 Fix 9 critical assert statements and RatVal division by zero (Priority 1) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
49d41272d9 Remove assertion for number of watches in normalize 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
c946207e23 Fix BOUNDS and ASSERT_FAIL issues in Python API 
- Add negative index support to AstVector.__setitem__, ModelRef.__getitem__, ApplyResult.__getitem__
- Replace bare assertions with proper Z3Exception in z3num.Numeral methods
- All changes tested and validated with comprehensive test suite

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
07c639a422 #8552 
make it recompile constraints with duplicates
 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
c031058978 small update to testing on p.m_sls_worker instead of should_run_sls 2026-02-18 21:02:22 -08:00
Copilot
730a54a767 Eliminate unnecessary copy operations in function parameters and range-based loops (#8589) 2026-02-18 21:02:22 -08:00
Nuno Lopes
f6f8beaf78 Remove copies (#8583) 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
776976cbd1 fix #8572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:20 -08:00
Nikolaj Bjorner
88a2a82898 fix #8552 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:20 -08:00
Nikolaj Bjorner
05e8e4a37c fix another regression by Nuno's changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:19 -08:00
Lev Nachmanson
24f3cddaac relax a too strong assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 21:02:19 -08:00
Copilot
62030bfddd Simplify svector assignment operators using = default (#8566) 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:19 -08:00
Nikolaj Bjorner
dcd8ea4af2 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:18 -08:00
Nuno Lopes
23a0a529fb revert swap changes to fix CI 2026-02-18 21:02:18 -08:00
Nikolaj Bjorner
c8cd205207 fix build warnings and scoop up after Nuno's leaks 2026-02-18 21:02:18 -08:00
Nuno Lopes
bbb29911f3 fix crash 2026-02-18 21:02:17 -08:00
Nuno Lopes
9152013fbd remove a few copies 2026-02-18 21:02:17 -08:00
Nuno Lopes
a3e7bbb92f replace some copies with moves 2026-02-18 21:02:17 -08:00
Nikolaj Bjorner
6b28d65487 set random seed directly on m_smt_params before context initialization 
updates to random seed on ctx does not get propagated to arithmetic solver, preventing diversity within arithmetic solver.
 2026-02-18 21:02:17 -08:00
Nuno Lopes
bfc132a4fc move, dont copy 2026-02-18 21:02:17 -08:00
Nuno Lopes
b7bf23c3bb move, dont copy 2026-02-18 21:02:17 -08:00
Copilot
58431ec158 Replace user-defined swap with C++11 move semantics for covert move patterns (#8543) 2026-02-18 21:02:17 -08:00
Lev Nachmanson
4c43bf585d fix the logic of adding all coefficients and blocking double insertions in m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 21:02:16 -08:00
Nikolaj Bjorner
0be8deefd3 Revert "mpz: use pointer tagging to save space (#8447)" 
This reverts commit 2f4abe2ce6.
 2026-02-18 21:02:16 -08:00
copilot-swe-agent[bot]
51fd4b2806 Fix OCaml linker flag and align validation runners with build runners 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:15 -08:00
copilot-swe-agent[bot]
3c401f186b Fix CMake variable name and clarify test path documentation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:15 -08:00
copilot-swe-agent[bot]
3ae8d7026a Apply headerpad fix to build systems (Python and CMake) and fix validation test paths 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:10 -08:00
Copilot
0761e91e8f Remove unused swap() methods (#8538) 2026-02-18 20:58:08 -08:00
Lev Nachmanson
f0c3a5bbb6 fix nlsat_explain.cpp that the regression tests would pass with lws=false 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:58:07 -08:00
copilot-swe-agent[bot]
d3c388a489 Add -headerpad_max_install_names flag for macOS dylib builds 
This fixes the install_name_tool issue on macOS where the tool fails
with "larger updated load commands do not fit". The linker flag
-Wl,-headerpad_max_install_names ensures sufficient header padding
in the Mach-O binary for install_name_tool to modify install names.

Changes made:
- CMake: Added flag to libz3, z3java, z3jl shared libraries on Darwin
- Python build: Changed flag from ML-only to all macOS builds
- OCaml CMake: Added flag to OCaml stublib build on APPLE

Fixes #7623 (regression in 4.15.5)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:07 -08:00
Copilot
3a8b688008 Store rational by value in parameter variant (#8518) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:07 -08:00
Nuno Lopes
e73c897bd4 constructor 2026-02-18 20:58:07 -08:00
Copilot
70626ac914 mpz: use pointer tagging to save space (#8447) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:07 -08:00
Nuno Lopes
1fa430479f remove redundant assert 2026-02-18 20:58:07 -08:00
copilot-swe-agent[bot]
38661f25e4 Fix build warnings: cast size_t to unsigned in arith_decl_plugin.h and bv_decl_plugin.h 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:07 -08:00
Lev Nachmanson
784c510bd5 Revert "optionally throttle patch_basic_columns() especially useful in unsat cases" 
This reverts commit bee2b45743.
 2026-02-18 20:58:06 -08:00
Lev Nachmanson
6351b612fc Revert "try fixed int patch period" 
This reverts commit 3e2027ec11.
 2026-02-18 20:58:06 -08:00
copilot-swe-agent[bot]
af5135274d Fix TypeScript compilation error: add updateField to Context interface 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:06 -08:00
copilot-swe-agent[bot]
8af4983863 Add datatype_update_field to C++, Python, TypeScript, and OCaml bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:06 -08:00
copilot-swe-agent[bot]
119008b46f Fix all build warnings with surgical changes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:05 -08:00
copilot-swe-agent[bot]
999a92e3e6 Revert prexpr to non-static for debugging availability 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:05 -08:00
copilot-swe-agent[bot]
21fd199062 Add static linkage to internal functions 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:05 -08:00
Lev Nachmanson
edc2715aa8 try fixed int patch period 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:58:05 -08:00
Copilot
b0b33367ef Add static linkage to inline functions in header files (#8519) 2026-02-18 20:58:05 -08:00
Lev Nachmanson
99bb57cb25 optionally throttle patch_basic_columns() especially useful in unsat cases 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:58:05 -08:00
Copilot
adf72f2a66 Modern C++: Add std::span overload for mk_or, adopt std::clamp, optimize stream output (#8507) 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:05 -08:00