mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity
22421 commits 71 branches 58 tags 220 MiB
Commit graph

22421 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
2a142cd150 recompile aw 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-11 10:12:03 -07:00
CEisenhofer
e584895c98 Make model extraction a bit more stable 2026-04-10 18:15:06 +02:00
CEisenhofer
2b7204b07c Does model construction work properly now? 2026-04-10 17:59:16 +02: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
CEisenhofer
598e4ede4e Removed debug code 2026-04-09 11:03:18 +02: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
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
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
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