mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-08 06:14:52 +00:00
Code Activity
20806 commits 46 branches 58 tags 222 MiB
Commit graph

20806 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
fa73827d98 fixes 2026-02-17 09:50:48 +00:00
Nuno Lopes
1a189ebdd7 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
ac748d973c fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
bd993ca963 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
0a22332196 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
dad012ad5d fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
4cdbe221cf fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
92158ac607 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
e9556c498b fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
8ce362abda fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
5f429d1223 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
88242fb4ce fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
9448f67d21 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
1c5cbcbe92 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
67ce05c1f5 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
10f986ee1a fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
8562788ad8 fixes 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
45f5209c23 Add out-of-line definitions for static constexpr members to fix ODR violations 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
227e48c0b1 Fix SMALL_BITS constant reference to use direct calculation instead 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
4941ef138b Fix undefined behavior when negating SMALL_INT_MIN in power_of_two_multiple 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
cd699ca582 Fix remaining int truncation issues in is_power_of_two, power_of_two_multiple, and log2 for 64-bit platforms 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
9bf691f8bd Refactor decompose function and consolidate value()/value64() into single value() returning int64_t 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
10c82a3b84 Fix machine_div2k to not truncate when result doesn't fit in small (add assertion instead) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
a5e1fa9930 Fix more uses of value() that should use value64() for 64-bit correctness 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
76dde47c4e Fix uses of value() that should be value64() for 64-bit small integers 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
5edef9e9a0 Remove nonsensical assertion and revert to simpler shift for SMALL_INT constants 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
dcfeb559fe Add assertion to set() method and simplify get_sign_cell by removing redundant SMALL_INT_MIN case 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
4dc74e2e30 Fix undefined behavior in SMALL_INT_MAX/MIN constants by using unsigned arithmetic 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
b8ed45bfac Revert deallocation in set methods and restore indentation in gcd function 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
6faaf86dca Implement proper bounds checking for small integers based on platform pointer size 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
copilot-swe-agent[bot]
cb3b8603eb Fix syntax errors in mpz.h 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
Nuno Lopes
ac1bef0053 mpz: use pointer tagging to save space (#8447) 
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
copilot-swe-agent[bot]
d8abd04a48 Initial plan 2026-02-17 09:50:47 +00:00
Nikolaj Bjorner
cff06b528f fix #8563 - align indices for flat quantifiers with sks vector layout, and also guard creating instantiation equalities with sort checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 20:57:38 -08:00
Nikolaj Bjorner
c0e8698bae
Merge pull request #8668 from Z3Prover/copilot/fix-build-warnings 
Fix C4267 warnings in ast.h initializer_list overloads
 2026-02-16 20:50:47 -08:00
copilot-swe-agent[bot]
037a4aa155 Fix C4267 build warnings in ast.h by adding static_cast for size_t to unsigned conversions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:44:23 +00:00
Nikolaj Bjorner
6884ffdd07
Merge pull request #8667 from Z3Prover/copilot/fix-a3-python-workflow-error 
Fix shell substitution breaking agentic workflow template interpolation
 2026-02-16 20:28:05 -08:00
copilot-swe-agent[bot]
9d8f736270 Initial plan 2026-02-17 04:27:04 +00:00
copilot-swe-agent[bot]
23d6262f7d Fix shell substitution in a3-python-v2 workflow as well 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:16:11 +00:00
copilot-swe-agent[bot]
f28b7ce440 Remove problematic shell substitution from a3-python workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:15:41 +00:00
copilot-swe-agent[bot]
a467a49453 Initial plan: Fix a3-python.md workflow shell substitution issue 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:15:08 +00:00
copilot-swe-agent[bot]
5da2b4ec19 Initial plan 2026-02-17 04:10:45 +00:00
Nikolaj Bjorner
27f11c8e76
Merge pull request #8664 from Z3Prover/copilot/simplify-go-bindings-code 
Simplify Go bindings: use astVectorToExprs helper in GetLowerAsVector/GetUpperAsVector
 2026-02-16 20:08:47 -08:00
copilot-swe-agent[bot]
5a9f416837 Simplify Go bindings: refactor GetLowerAsVector and GetUpperAsVector to use astVectorToExprs helper 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 03:46:58 +00:00
copilot-swe-agent[bot]
966e651b8b Initial plan 2026-02-17 03:44:53 +00:00
Nikolaj Bjorner
f9daab94d4
Merge pull request #8658 from Z3Prover/dependabot/github_actions/githubnext/gh-aw-0.45.1 
Bump githubnext/gh-aw from 0.42.17 to 0.45.1
 2026-02-16 19:40:30 -08:00
Nikolaj Bjorner
5c41b93498
Merge pull request #8659 from Z3Prover/dependabot/github_actions/actions/download-artifact-7.0.0 
Bump actions/download-artifact from 6.0.0 to 7.0.0
 2026-02-16 19:40:15 -08:00
Nikolaj Bjorner
88b004b5b6
Merge pull request #8660 from Z3Prover/dependabot/github_actions/actions/checkout-6.0.2 
Bump actions/checkout from 5.0.1 to 6.0.2
 2026-02-16 19:34:55 -08:00
Nikolaj Bjorner
86a12f4836
Merge pull request #8661 from Z3Prover/dependabot/github_actions/github/gh-aw-0.45.1 
Bump github/gh-aw from 0.43.15 to 0.45.1
 2026-02-16 19:34:43 -08:00
Nikolaj Bjorner
8eed390a6c
Merge pull request #8662 from Z3Prover/dependabot/github_actions/actions/cache-5.0.3 
Bump actions/cache from 4.3.0 to 5.0.3
 2026-02-16 19:34:29 -08:00