mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-11 17:46:20 +00:00
Code Activity
22958 commits 97 branches 58 tags 279 MiB
Commit graph

22958 commits

This branch
This branch
All branches
Author SHA1 Message Date
CEisenhofer
a81ce477f5 Added classical regex factorization 2026-04-02 20:08:00 +02:00
Nikolaj Bjorner
3ca960d679 test that there is a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 10:49:09 -07:00
Nikolaj Bjorner
b0a4a15c98 updated tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 10:04:02 -07:00
CEisenhofer
34cb0a17fc str.at wants a special treatment... 2026-04-02 18:33:44 +02:00
Copilot
8d7ed66ebf
Fix Specbot Crash Analyzer: move Z3 build to pre-steps to avoid MCP session timeout (#9200) 
* Initial plan

* Fix specbot-crash-analyzer: move build to pre-steps to avoid MCP session timeout

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/add5e714-bc98-44cf-ad6b-5adfbe4668c3

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>
 2026-04-02 08:48:25 -07:00
CEisenhofer
a8db876765 Fix problem with divisibility predicate 2026-04-02 16:25:49 +02:00
CEisenhofer
5ec28d3bc8 Eliminate length gradients from regexes 2026-04-02 15:58:15 +02:00
CEisenhofer
1282e4de11 Prevent unsoudness because of missing length propagation 2026-04-02 14:34:46 +02:00
CEisenhofer
1e567a4a26 Bug fixes 2026-04-02 10:26:36 +02:00
Copilot
eef00e2023
Add specbot-crash-analyzer agentic workflow (.md + .lock.yml) (#9198) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/efdf69c9-8aca-4acc-b780-f3a7769ba116

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-04-02 01:10:56 -07:00
Nikolaj Bjorner
4c463ad813 add report 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 00:48:27 -07:00
Nikolaj Bjorner
251127e45f add specbot tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 00:44:47 -07:00
Nikolaj Bjorner
2245451e96 remove aux function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 19:07:37 -07:00
Nikolaj Bjorner
6e8c201234 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 16:00:01 -07:00
Nikolaj Bjorner
d05dccf331 add current_value access 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 13:30:15 -07:00
Nikolaj Bjorner
b1dc2f2be2 It is possible that a non-internalized expression gets assigned to false immediately by internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 11:49:25 -07:00
CEisenhofer
42f421ee09 Detect that adding side constraint caused a conflict 2026-04-01 20:38:15 +02:00
Nikolaj Bjorner
4524ebe614 fix type error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 10:35:10 -07:00
CEisenhofer
f709f6d089 Don't add constraint twice 2026-04-01 18:56:45 +02:00
CEisenhofer
261385f702 Merge remote-tracking branch 'origin/c3' into c3 2026-04-01 18:51:36 +02:00
Nikolaj Bjorner
9a29a0fc24 hoist functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 09:41:49 -07:00
Nikolaj Bjorner
3879e2190a recompile workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 09:27:45 -07:00
Copilot
cf051598f9
Update RELEASE_NOTES.md with Version 4.17.0 additions from discussion #9172 (#9186) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/488739ce-e615-410e-8956-677db4c0df2a

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-04-01 08:54:45 -07:00
Nikolaj Bjorner
5f5a0ffbd8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 08:47:56 -07:00
Nikolaj Bjorner
f5382144e6 use mod counts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 08:41:49 -07:00
Nikolaj Bjorner
3ad6df3258 build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 08:29:41 -07:00
CEisenhofer
beda426d7c Integer conflicts are proper conflicts 2026-04-01 17:21:11 +02:00
CEisenhofer
36b01a51f1 Properly extract justifications from subsolver 2026-04-01 16:58:26 +02:00
Copilot
7f9494329f
Refactor: Add arith_util a member to nielsen_graph, eliminate repeated local instantiations (#9185) 
* add arith_util a attribute to nielsen_graph, replace local arith_util instances

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/8d6c7e3f-5853-4c64-a448-34a10fb64f3b

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* remove arith aliases, reference a directly in nielsen_graph methods

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/a6a64bf1-86fc-41bc-a245-2f67656d5f63

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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-01 07:18:23 -07:00
CEisenhofer
e25e93503b First try to do better dependency tracking 2026-04-01 15:23:38 +02:00
CEisenhofer
60913f0068 Output both Nielsen graph size and conflict size 2026-04-01 10:23:55 +02:00
CEisenhofer
5d95f44a03 Conflict logging 2026-04-01 10:08:03 +02:00
Nikolaj Bjorner
1f8773ea7d nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-31 20:12:59 -07:00
Nikolaj Bjorner
2cec2dadf9 cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-31 18:30:59 -07:00
Nikolaj Bjorner
013d6b3063 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-31 18:21:38 -07:00
Nikolaj Bjorner
860bd43559 remove reference to arith_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-31 16:16:53 -07:00
Copilot
56a8259717
Add Z3_mk_polymorphic_datatype to Python, .NET, Go, and TypeScript bindings (#9181) 
* Add Z3_mk_polymorphic_datatype to Python, .NET, Go, and TypeScript bindings

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/13ef481d-61f5-47e1-8659-59cd91692fdd

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Improve Python error message for polymorphic datatype self-reference check

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/13ef481d-61f5-47e1-8659-59cd91692fdd

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>
 2026-03-31 14:15:34 -07:00
Copilot
56eeb5b52c
Add pseudo-Boolean/cardinality constraints to Go and OCaml APIs (#9182) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/64ff2e48-47b1-4195-b154-ac38095dbbfb

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-31 13:44:52 -07:00
Copilot
31425b07ca
Add SetGlobalParam, GetGlobalParam, ResetAllGlobalParams to Go bindings (#9179) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f06c74eb-4cac-45f6-92b9-b2698150074c

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-31 09:48:37 -07:00
Yanjun Yang(Pluto)
ba77141b51
add tag for linux/loongarch64 (#9184) 2026-03-31 08:57:20 -07:00
Nikolaj Bjorner
7ec3f7f107 add split function for unit_regex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-31 08:56:36 -07:00
CEisenhofer
14f71ea852 Reuse power variables and symbolic characters 2026-03-31 16:36:10 +02:00
Lev Nachmanson
1ec07ac5e9 restore an optimization in scoped_numeral_vector.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-03-30 19:53:23 -10:00
Nikolaj Bjorner
54d52d882f remove indirect references to ast_manager 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-30 20:00:02 -07:00
dependabot[bot]
4ece18c284
Bump github/gh-aw from 0.57.2 to 0.65.0 (#9173) 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 0.57.2 to 0.65.0.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Commits](https://github.com/github/gh-aw/compare/v0.57.2...v0.65.0)

---
updated-dependencies:
- dependency-name: github/gh-aw
  dependency-version: 0.65.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-30 19:17:19 -07:00
dependabot[bot]
a988457b0a
Bump actions/download-artifact from 8.0.0 to 8.0.1 (#9174) 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 8.0.0 to 8.0.1.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v8...v8.0.1)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: 8.0.1
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-30 19:17:06 -07:00
dependabot[bot]
826b15e320
Bump nuget/setup-nuget from 2 to 3 (#9175) 
Bumps [nuget/setup-nuget](https://github.com/nuget/setup-nuget) from 2 to 3.
- [Release notes](https://github.com/nuget/setup-nuget/releases)
- [Commits](https://github.com/nuget/setup-nuget/compare/v2...v3)

---
updated-dependencies:
- dependency-name: nuget/setup-nuget
  dependency-version: '3'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-30 19:16:54 -07:00
dependabot[bot]
f8720c9ce3
Bump actions/cache from 5.0.3 to 5.0.4 (#9176) 
Bumps [actions/cache](https://github.com/actions/cache) from 5.0.3 to 5.0.4.
- [Release notes](https://github.com/actions/cache/releases)
- [Commits](https://github.com/actions/cache/compare/v5.0.3...v5.0.4)

---
updated-dependencies:
- dependency-name: actions/cache
  dependency-version: 5.0.4
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-03-30 19:16:39 -07:00
Nikolaj Bjorner
6d2321e6fe edits to seq_nielsen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-30 17:36:27 -07:00
Lev Nachmanson
b3f977d06c
Fix nlsat clear crash (#9150) 
* fix nlsat clear() and scoped_numeral_vector copy ctor crashes

Reset polynomial cache and assignments in nlsat::solver:👿:clear()
to prevent use-after-free when the solver is destroyed. The missing
resets caused heap corruption when check_assignment's
compute_linear_explanation created cached polynomials and root atoms
that outlived the solver's other data structures during destruction.

Also fix _scoped_numeral_vector copy constructor to read from other
instead of uninitialized self.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* simplify scoped_numeral_vector copy constructor loop

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* revert clear() additions that cause heap corruption

The m_cache.reset(), m_assignment.reset(), m_lo.reset(), m_hi.reset()
calls added to clear() in commit 481eb0327 cause heap corruption when
clear() is called from the destructor. The cache reset frees polynomials
while the polynomial manager still holds references to them, corrupting
the heap. This manifests as 'corrupted double-linked list' crashes
during nlsat solver destruction in the nra check path.

The reset() method already has these calls for solver reuse. The
destructor path via clear() should not duplicate them, as implicit
member destruction handles cleanup in the correct order.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* fix heap corruption from root_function move/sort operations

root_function's move constructor and move assignment were doing deep
copies of algebraic numbers via anum_manager::set() instead of proper
moves. During std::vector reallocation (emplace) and std::sort, this
caused massive allocation churn that corrupted the heap.

Fixes:
1. Move constructor: use std::move(other.val) for proper swap semantics.
2. Move assignment: use val.swap(other.val) instead of deep copy.
3. Add friend swap() for ADL so std::sort uses efficient swaps.
4. Sort root_function partitions via index permutation + swap cycles
   instead of std::sort directly on root_function objects.
5. Reserve rfunc vector before emplace in add_linear_approximations().
6. Reserve lhalf/uhalf vectors before collecting root functions.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* Fix apply_permutation to take perm by const reference

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f81ba8ad-2875-4fcc-ba91-d502905756be

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
 2026-03-30 04:58:45 -10:00