3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-10 14:35:33 +00:00

Commit graph

  • 9b3826ed86 Missing case in concatenation CEisenhofer 2026-04-02 20:07:51 +02:00
  • a81ce477f5 Added classical regex factorization CEisenhofer 2026-04-02 20:03:22 +02:00
  • 3ca960d679 test that there is a model Nikolaj Bjorner 2026-04-02 10:49:09 -07:00
  • b0a4a15c98 updated tests Nikolaj Bjorner 2026-04-02 10:03:29 -07:00
  • a87095f931
    Fix specbot test harness for POSIX/Linux compatibility copilot-swe-agent[bot] 2026-04-02 16:44:21 +00:00
  • 8e165e14c0
    Add specbot test files from c3 branch copilot-swe-agent[bot] 2026-04-02 16:42:19 +00:00
  • 34cb0a17fc str.at wants a special treatment... CEisenhofer 2026-04-02 18:33:44 +02:00
  • 8d7ed66ebf
    Fix Specbot Crash Analyzer: move Z3 build to pre-steps to avoid MCP session timeout (#9200) copilot/apply-suggested-fixes-to-tests Copilot 2026-04-02 08:48:25 -07:00
  • a8db876765 Fix problem with divisibility predicate CEisenhofer 2026-04-02 16:25:49 +02:00
  • 5ec28d3bc8 Eliminate length gradients from regexes CEisenhofer 2026-04-02 15:58:15 +02:00
  • 1282e4de11 Prevent unsoudness because of missing length propagation CEisenhofer 2026-04-02 14:34:46 +02:00
  • 3c3ba969d7
    Fix specbot-crash-analyzer: move build to pre-steps to avoid MCP session timeout copilot-swe-agent[bot] 2026-04-02 09:37:52 +00:00
  • bf195422fb
    Initial plan copilot-swe-agent[bot] 2026-04-02 09:26:22 +00:00
  • 1e567a4a26 Bug fixes CEisenhofer 2026-04-02 10:26:36 +02:00
  • eef00e2023
    Add specbot-crash-analyzer agentic workflow (.md + .lock.yml) (#9198) Copilot 2026-04-02 01:10:56 -07:00
  • 95cac0668e
    Add specbot-crash-analyzer agentic workflow (.md + .lock.yml) copilot-swe-agent[bot] 2026-04-02 07:51:57 +00:00
  • 4c463ad813 add report Nikolaj Bjorner 2026-04-02 00:48:27 -07:00
  • 251127e45f add specbot tests Nikolaj Bjorner 2026-04-02 00:44:47 -07:00
  • 2245451e96 remove aux function Nikolaj Bjorner 2026-04-01 19:07:37 -07:00
  • 6e8c201234 fix test Nikolaj Bjorner 2026-04-01 16:00:01 -07:00
  • 008a101c08
    seq_eq_solver: add pointer-equality fast path in has_len_offset and use all_of in find_branch_candidate copilot-swe-agent[bot] 2026-04-01 22:08:19 +00:00
  • ec495c094c
    seq_ne_solver: short-circuit propagate_ne2eq for str.unit elements copilot-swe-agent[bot] 2026-04-01 22:06:52 +00:00
  • fd28976f4c
    Initial plan copilot-swe-agent[bot] 2026-04-01 21:50:27 +00:00
  • 57fdf43475
    Initial plan copilot-swe-agent[bot] 2026-04-01 21:49:11 +00:00
  • d05dccf331 add current_value access Nikolaj Bjorner 2026-04-01 13:30:15 -07:00
  • b1dc2f2be2 It is possible that a non-internalized expression gets assigned to false immediately by internalization Nikolaj Bjorner 2026-04-01 11:48:15 -07:00
  • 42f421ee09 Detect that adding side constraint caused a conflict CEisenhofer 2026-04-01 20:38:15 +02:00
  • 4524ebe614 fix type error Nikolaj Bjorner 2026-04-01 10:34:20 -07:00
  • 4f5c19acfa remove unused functions from seq_nielsen copilot-swe-agent[bot] 2026-04-01 17:16:12 +00:00
  • f709f6d089 Don't add constraint twice CEisenhofer 2026-04-01 18:56:45 +02:00
  • 261385f702 Merge remote-tracking branch 'origin/c3' into c3 CEisenhofer 2026-04-01 18:51:36 +02:00
  • 9a29a0fc24 hoist functionality Nikolaj Bjorner 2026-04-01 09:41:49 -07:00
  • 3879e2190a recompile workflows Nikolaj Bjorner 2026-04-01 09:27:45 -07:00
  • cf051598f9
    Update RELEASE_NOTES.md with Version 4.17.0 additions from discussion #9172 (#9186) Copilot 2026-04-01 08:54:45 -07:00
  • 5f5a0ffbd8 na Nikolaj Bjorner 2026-04-01 08:47:56 -07:00
  • f5382144e6 use mod counts Nikolaj Bjorner 2026-04-01 08:41:49 -07:00
  • 3ad6df3258 build fixes Nikolaj Bjorner 2026-04-01 08:29:41 -07:00
  • beda426d7c Integer conflicts are proper conflicts CEisenhofer 2026-04-01 17:21:11 +02:00
  • 36b01a51f1 Properly extract justifications from subsolver CEisenhofer 2026-04-01 16:58:26 +02:00
  • 7f9494329f
    Refactor: Add arith_util a member to nielsen_graph, eliminate repeated local instantiations (#9185) Copilot 2026-04-01 07:18:23 -07:00
  • 76ea0d2fbf
    Merge branch 'c3' into copilot/add-arith-util-to-nielsen-graph Nikolaj Bjorner 2026-04-01 07:18:09 -07:00
  • e25e93503b First try to do better dependency tracking CEisenhofer 2026-04-01 15:23:38 +02:00
  • 60913f0068 Output both Nielsen graph size and conflict size CEisenhofer 2026-04-01 10:23:55 +02:00
  • 5d95f44a03 Conflict logging CEisenhofer 2026-04-01 10:08:03 +02:00
  • f12ee63ff5 remove arith aliases, reference a directly in nielsen_graph methods copilot-swe-agent[bot] 2026-04-01 03:47:31 +00:00
  • 186448446f Update RELEASE_NOTES.md with Version 4.17.0 additions from discussion #9172 copilot-swe-agent[bot] 2026-04-01 03:33:09 +00:00
  • 1f8773ea7d nits Nikolaj Bjorner 2026-03-31 20:12:59 -07:00
  • 8f90ae01a6 add arith_util a attribute to nielsen_graph, replace local arith_util instances copilot-swe-agent[bot] 2026-04-01 02:58:04 +00:00
  • 2cec2dadf9 cleanup Nikolaj Bjorner 2026-03-31 18:30:59 -07:00
  • 013d6b3063 na Nikolaj Bjorner 2026-03-31 18:21:38 -07:00
  • 860bd43559 remove reference to arith_solver Nikolaj Bjorner 2026-03-31 16:16:53 -07:00
  • 56a8259717
    Add Z3_mk_polymorphic_datatype to Python, .NET, Go, and TypeScript bindings (#9181) Copilot 2026-03-31 14:15:34 -07:00
  • 367ae39a50 fix CI: add set_lower/upper_int_bound to nielsen_node, fix nseq_basic simplify_and_init call copilot-swe-agent[bot] 2026-03-31 21:05:44 +00:00
  • 56eeb5b52c
    Add pseudo-Boolean/cardinality constraints to Go and OCaml APIs (#9182) Copilot 2026-03-31 13:44:52 -07:00
  • 9d152d5248 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. Ilana Shapiro 2026-03-31 12:33:24 -07:00
  • 31425b07ca
    Add SetGlobalParam, GetGlobalParam, ResetAllGlobalParams to Go bindings (#9179) Copilot 2026-03-31 09:48:37 -07:00
  • 587400bc3d
    Update seq_nielsen.cpp Nikolaj Bjorner 2026-03-31 09:30:48 -07:00
  • 310eee1782
    Update seq_nielsen.cpp Nikolaj Bjorner 2026-03-31 09:04:32 -07:00
  • ce8d770745
    Merge branch 'c3' into copilot/port-modifier-regexcharsplitmodifier Nikolaj Bjorner 2026-03-31 09:03:30 -07:00
  • ba77141b51
    add tag for linux/loongarch64 (#9184) Yanjun Yang(Pluto) 2026-03-31 23:57:20 +08:00
  • 7ec3f7f107 add split function for unit_regex Nikolaj Bjorner 2026-03-31 08:56:31 -07:00
  • 14f71ea852 Reuse power variables and symbolic characters CEisenhofer 2026-03-31 16:36:10 +02:00
  • ec898aff3c apply_regex_unit_split: use decompose_ite loop instead of get_cofactors copilot-swe-agent[bot] 2026-03-31 11:32:02 +00:00
  • bbbf826f30 add tag for linux/loongarch64 Pluto Yang 2026-03-31 16:31:27 +08:00
  • 1ec07ac5e9 restore an optimization in scoped_numeral_vector.h Lev Nachmanson 2026-03-30 19:53:23 -10:00
  • 6e6f4ad4ed apply_regex_unit_split: use co-factor derivative approach instead of minterms copilot-swe-agent[bot] 2026-03-31 03:38:40 +00:00
  • 54d52d882f remove indirect references to ast_manager Nikolaj Bjorner 2026-03-30 20:00:02 -07:00
  • 4b08c629c8 port RegexCharSplitModifier: implement apply_regex_unit_split in seq_nielsen copilot-swe-agent[bot] 2026-03-31 02:51:21 +00:00
  • 648b9a1bc2
    Merge branch 'master' into runner-guard/fix-ci-security Nikolaj Bjorner 2026-03-30 19:27:31 -07:00
  • 4ece18c284
    Bump github/gh-aw from 0.57.2 to 0.65.0 (#9173) dependabot[bot] 2026-03-30 19:17:19 -07:00
  • a988457b0a
    Bump actions/download-artifact from 8.0.0 to 8.0.1 (#9174) dependabot[bot] 2026-03-30 19:17:06 -07:00
  • 826b15e320
    Bump nuget/setup-nuget from 2 to 3 (#9175) dependabot[bot] 2026-03-30 19:16:54 -07:00
  • f8720c9ce3
    Bump actions/cache from 5.0.3 to 5.0.4 (#9176) dependabot[bot] 2026-03-30 19:16:39 -07:00
  • 4379733c83 Improve Python error message for polymorphic datatype self-reference check copilot-swe-agent[bot] 2026-03-31 00:57:20 +00:00
  • 7908a62578 Add Z3_mk_polymorphic_datatype to Python, .NET, Go, and TypeScript bindings copilot-swe-agent[bot] 2026-03-31 00:53:20 +00:00
  • 749f161302 feat: add Z3_mk_type_variable to .NET, TypeScript, and C++ bindings copilot-swe-agent[bot] 2026-03-31 00:45:18 +00:00
  • 54beb2411c Add pseudo-Boolean/cardinality constraints to Go and OCaml APIs copilot-swe-agent[bot] 2026-03-31 00:43:04 +00:00
  • 3cfd1538bd Add SetGlobalParam, GetGlobalParam, ResetAllGlobalParams to Go bindings copilot-swe-agent[bot] 2026-03-31 00:41:39 +00:00
  • 6d2321e6fe edits to seq_nielsen Nikolaj Bjorner 2026-03-30 17:36:27 -07:00
  • 7ca3b111e8
    Bump actions/cache from 5.0.3 to 5.0.4 dependabot[bot] 2026-03-30 22:47:02 +00:00
  • 4a071aa436
    Bump nuget/setup-nuget from 2 to 3 dependabot[bot] 2026-03-30 22:46:35 +00:00
  • 1fcc40d0ec
    Bump actions/download-artifact from 8.0.0 to 8.0.1 dependabot[bot] 2026-03-30 22:46:30 +00:00
  • a516f3ebe9
    Bump github/gh-aw from 0.57.2 to 0.65.0 dependabot[bot] 2026-03-30 22:46:00 +00:00
  • b3f977d06c
    Fix nlsat clear crash (#9150) Lev Nachmanson 2026-03-30 04:58:45 -10:00
  • 1f506ee242 Fix apply_permutation to take perm by const reference copilot-swe-agent[bot] 2026-03-29 03:19:57 +00:00
  • 20548c08ec fix heap corruption from root_function move/sort operations Lev Nachmanson 2026-03-28 04:57:44 -10:00
  • e760eabd2b revert clear() additions that cause heap corruption Lev Nachmanson 2026-03-27 20:01:04 -10:00
  • 78d70fea37 simplify scoped_numeral_vector copy constructor loop Lev Nachmanson 2026-03-27 15:31:52 -10:00
  • 75baedb314 fix nlsat clear() and scoped_numeral_vector copy ctor crashes Lev Nachmanson 2026-03-27 11:09:19 -10:00
  • 9aceaf3cac reviewing seq_nielsen, detect repeated final-check to avoid rebuilding nielsen graph Nikolaj Bjorner 2026-03-30 00:01:24 -07:00
  • c1112d430f Remove old tactic class, use simplifier-backed mk_bv_size_reduction_tactic copilot-swe-agent[bot] 2026-03-30 03:43:03 +00:00
  • a79a48ed2a add comment about fresh variable Nikolaj Bjorner 2026-03-29 20:16:07 -07:00
  • 684cb23b40 turn on constraint integrity checking Nikolaj Bjorner 2026-03-29 19:30:13 -07:00
  • d7ee475bc3 ensure equalities are propagated Nikolaj Bjorner 2026-03-29 16:47:05 -07:00
  • 6d31bdcc21 use sk.mk_seq_eq to avoid disequality propagations Nikolaj Bjorner 2026-03-29 15:45:42 -07:00
  • 09cde1f80c
    Port propagate_eq from theory_seq for sk().is_eq in theory_nseq (#9165) Copilot 2026-03-29 15:44:18 -07:00
  • e8a144120c Port propagate_eq from theory_seq for sk().is_eq in theory_nseq copilot-swe-agent[bot] 2026-03-29 22:40:46 +00:00
  • 3db734d249 add note about propagate-eq Nikolaj Bjorner 2026-03-29 15:19:36 -07:00
  • f9b6d64e0b
    Fix apply_permutation to take perm by const reference copilot-swe-agent[bot] 2026-03-29 03:19:57 +00:00
  • 398e269d43 fix: pin 18 unpinned action(s), extract 26 unsafe expression(s) to env vars dagecko 2026-03-28 19:56:44 -04:00