mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-25 18:10:35 +00:00
Code Activity
22747 commits 83 branches 58 tags 266 MiB
Commit graph

22747 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ilana Shapiro
ceb363d35d
SMTS tree algorithms (#9250) 
* Refactor parallel search tree to use global node selection (SMTS-style) instead of DFS traversal.
Introduce effort-based prioritization, allow activation of any open node, and add controlled/gated
expansion to prevent over-partitioning and improve load balancing.

* clean up code

* ablations

* ablations2: effort

* ablations2: activation

* ablations3: more activations

* ablations4: visit all nodes before splitting

* throttle tree size min is based on workers not activated nodes

* ablate random throttling

* ablate nonlinear effort

* clean up code

* ablate throttle

* ablate where add_effort is

* reset

* clean up a function and add comment

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
 2026-04-09 09:46:47 -07:00
Nikolaj Bjorner
c7879ed5ad fix #9254 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-09 09:19:40 -07:00
CEisenhofer
e6ef0d29c4 We need to check local consistency over and over again 2026-04-09 15:56:00 +02:00
CEisenhofer
09572b20ed Character ranges must be passed back to the solver 2026-04-09 15:21:12 +02:00
CEisenhofer
aafb704cf8 Bug fix in model extraction 2026-04-09 14:42:48 +02:00
CEisenhofer
d127055841 fix(nseq): handle empty children in apply_regex_factorization 2026-04-09 14:24:44 +02:00
CEisenhofer
a36254f104 Some more bug fixes 2026-04-09 13:47:29 +02:00
CEisenhofer
38d725dc5a Deriving by allchar should not crash 2026-04-09 11:48:35 +02:00
CEisenhofer
8eb0ac29d9 We have to check for local conflicts before clearing the flag 2026-04-09 11:42:30 +02:00
Nikolaj Bjorner
bb48e3a405 disable spurious test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-09 02:20:45 -07:00
CEisenhofer
598e4ede4e Removed debug code 2026-04-09 11:03:18 +02:00
Guangyu (Gary) HU
704dc9375d
mini_ic3: fix generalize() returning empty/init-overlapping core (#9245) 
Two fixes in examples/python/mini_ic3.py:

1. generalize(): the polarity of the disjointness check was inverted,
   and there was no guard against an empty unsat core. With an empty
   core, And([])=True so check_disjoint(init, prev(True)) is always
   False (init is sat), and the code returned the empty core. That
   empty core then became cube2clause([])=Or([])=False, which got
   added as a lemma to all frames. The frame became inconsistent and
   is_valid() returned And(Or())=False as the "inductive invariant".

   Fix: require len(core) > 0 AND check_disjoint(init, prev(core))
   (without the spurious 'not'), so the core is only used when it
   is genuinely disjoint from init.

2. is_transition(): when an init rule's body happens to be an And
   without any Invariant predicate (e.g. (and (not A) (not B) ...)),
   is_body() returns (And(...), None). is_transition then passed
   inv0=None to subst_vars() which crashed inside get_vars(). Add an
   explicit None check so the rule falls through to is_init().

Verified on horn1..5 (unchanged behavior), h_CRC and h_FIFO from the
blocksys benchmarks (now correctly return CEX matching z3 spacer),
and cache_coherence_three (no longer collapses to (and or)).
 2026-04-09 02:01:07 -07:00
dependabot[bot]
5d0141d916
Bump mymindstorm/setup-emsdk from 14 to 15 (#9242) 
Bumps [mymindstorm/setup-emsdk](https://github.com/mymindstorm/setup-emsdk) from 14 to 15.
- [Release notes](https://github.com/mymindstorm/setup-emsdk/releases)
- [Commits](https://github.com/mymindstorm/setup-emsdk/compare/v14...v15)

---
updated-dependencies:
- dependency-name: mymindstorm/setup-emsdk
  dependency-version: '15'
  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-04-09 02:00:17 -07:00
dependabot[bot]
9d078c4593
Bump github/gh-aw (#9241) 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 89ae1c2ebfae7f8233fa4bd6a83b1121f65dc376 to 17f01e1a5f75fa627fab7a800878bd14e29d8005.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Changelog](https://github.com/github/gh-aw/blob/main/CHANGELOG.md)
- [Commits](89ae1c2ebf...17f01e1a5f)

---
updated-dependencies:
- dependency-name: github/gh-aw
  dependency-version: 17f01e1a5f75fa627fab7a800878bd14e29d8005
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-04-09 01:59:54 -07:00
CEisenhofer
803018b7c3 We forgot relevant equations with one side being empty 2026-04-09 10:40:33 +02:00
CEisenhofer
684f93bed4 We should not stop eagerly on local conflicts 2026-04-08 20:13:54 +02:00
CEisenhofer
857e93fdb2 Substitutions are extensions 2026-04-08 19:13:10 +02:00
CEisenhofer
513f49f39c Debugging 2026-04-08 18:48:47 +02:00
CEisenhofer
86dc9d3268 We need to reset local conflicts 2026-04-08 18:24:11 +02:00
CEisenhofer
26ededa891 More debug info 2026-04-08 18:00:52 +02:00
CEisenhofer
74cf21b852 Bug in model extraction 
Added debug check
 2026-04-08 16:37:21 +02:00
CEisenhofer
26d36ba6ee Missing justification added 
Added check for correctness of conflict core
 2026-04-08 10:15:27 +02:00
CEisenhofer
c7e7b40d40 Fix 2026-04-08 09:27:46 +02:00
CEisenhofer
f895548154 Check for range conflicts for characters 2026-04-07 10:49:23 +02:00
CEisenhofer
1a1961be2f Removed tracking disequality 2026-04-07 10:33:44 +02:00
CEisenhofer
3e24cb7c10 Bug 2026-04-07 09:33:14 +02:00
Arie
477a1d817d
Add mod-factor-propagation lemma to NLA divisions solver (#9235) 
When a monic x*y has a factor x with mod(x, p) = 0 (fixed), propagate
mod(x*y, p) = 0. This enables Z3 to prove divisibility properties like
x mod p = 0 => (x*y) mod p = 0, which previously timed out even for
p = 2. The lemma fires in the NLA divisions check and allows Gröbner
basis and LIA to subsequently derive distributivity of div over addition.

Extends division tuples from (q, x, y) to (q, x, y, r) to track the
mod lpvar. Also registers bounded divisions from the mod internalization
path in theory_lra, not just the idiv path.

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
 2026-04-05 17:34:11 -07:00
CEisenhofer
2a32aa0204 fix(nseq): assert sub-sequence equalities to the SAT core 2026-04-04 19:11:36 +02:00
CEisenhofer
8298ba6011 Quick fix for some unsound cases 2026-04-04 18:36:25 +02:00
CEisenhofer
a58a9114d2 Fix str.< Skolem length generation overhead 2026-04-04 18:32:02 +02:00
Nikolaj Bjorner
b60a44c66b classical 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-03 10:33:28 -07:00
Nikolaj Bjorner
cdccd389e9 revert s_unknown 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-03 10:04:13 -07:00
Nikolaj Bjorner
95dc44b409 bugfix, better debug display of failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-03 09:08:22 -07:00
Copilot
fa89910452
Add SASSERT invariants and pre/postconditions to Nielsen seq solver (#9216) 
* Initial plan

* Add SASSERT invariants and pre/postconditions to Nielsen seq solver

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698

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

* Add clarifying comment to m_str_eq.empty() postcondition

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698

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 21:09:23 -07:00
Copilot
bbb704e63c
seq_axioms: eliminate redundant mk_literal call in add_clause (#9215) 
* Initial plan

* fix: use already-computed literal in seq_axioms::add_clause

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/0ab6afce-13a9-4e77-87b4-e416bc06f413

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 21:08:16 -07:00
Copilot
ddd8bf84d7
Replace apply_regex_unit_split with apply_regex_if_split (#9210) 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7df36402-f2c7-4de5-b626-3df14d4eee64

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 14:27:06 -07:00
Nikolaj Bjorner
e59ee306e9 allow literals to be false in model validation - we can't enforce lack of propagation after internalizing literals, especially if literals are repeated (modulo permutation of equality) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 12:51:47 -07:00
Nikolaj Bjorner
3629cd9447 regression fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-02 11:42:50 -07:00
CEisenhofer
9b3826ed86 Missing case in concatenation 2026-04-02 20:08:00 +02:00
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