3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-07 05:02:48 +00:00

Commit graph

  • 40e5cd502c
    Merge 843c9d9d29 into 477a1d817d dependabot[bot] 2026-04-06 22:17:29 +00:00
  • 843c9d9d29
    Bump mymindstorm/setup-emsdk from 14 to 15 dependabot/github_actions/mymindstorm/setup-emsdk-15 dependabot[bot] 2026-04-06 22:17:25 +00:00
  • 1d25857408
    Merge 76acce2c87 into 477a1d817d dependabot[bot] 2026-04-06 22:17:21 +00:00
  • 76acce2c87
    Bump github/gh-aw dependabot/github_actions/github/gh-aw-17f01e1a5f75fa627fab7a800878bd14e29d8005 dependabot[bot] 2026-04-06 22:17:16 +00:00
  • 229df16f9b
    Merge 8e8799dbd3 into 477a1d817d Don Syme 2026-04-06 10:29:54 +02:00
  • 8b7f2deecd
    Merge e6607df831 into 477a1d817d Copilot 2026-04-06 10:29:54 +02:00
  • 8fc6024b04
    Merge 6b12bffd55 into 477a1d817d Copilot 2026-04-06 10:29:54 +02:00
  • 21ab14542f
    Merge 9e96ee91dc into 477a1d817d Copilot 2026-04-06 10:29:54 +02:00
  • bfa34306ba
    Merge f0612ab7e0 into 477a1d817d Copilot 2026-04-06 10:29:54 +02:00
  • 056237fd28
    Merge d3f5fd6825 into 477a1d817d Lev Nachmanson 2026-04-06 10:29:54 +02:00
  • ab53acaf4a
    Merge c41753baad into 477a1d817d Copilot 2026-04-06 10:29:54 +02:00
  • b2a5954df9
    Merge a37003fa2d into 477a1d817d Lev Nachmanson 2026-04-06 10:29:54 +02:00
  • 53afbae832
    Merge a636fb3e83 into 477a1d817d Copilot 2026-04-06 10:20:55 +02:00
  • c43f323900
    Merge c49b403922 into 477a1d817d Copilot 2026-04-06 01:51:18 +00:00
  • c49b403922
    fstar: address code review comments - document gen_rhs_expr_list and strip-components copilot/formalize-fpa-rewrite-rules copilot-swe-agent[bot] 2026-04-06 01:51:11 +00:00
  • 4a2accf10c
    fstar: fix F* 2026 compatibility and run Meta-F* extraction successfully copilot-swe-agent[bot] 2026-04-06 01:49:41 +00:00
  • 477a1d817d
    Add mod-factor-propagation lemma to NLA divisions solver (#9235) master Nightly Arie 2026-04-05 20:34:11 -04:00
  • cf00de9c57 Add mod-factor-propagation lemma to NLA divisions solver Arie Gurfinkel 2026-04-05 14:24:33 -04:00
  • e5acaf0c28
    fstar: add extract.sh script and fstar-extract.yml GHA workflow for Meta-F* extraction copilot-swe-agent[bot] 2026-04-05 02:45:56 +00:00
  • da40b270a1
    fstar: address code review - diagnostic on bvar fallback, refactor extractions, fix include path copilot-swe-agent[bot] 2026-04-05 02:39:55 +00:00
  • e2ffbe8c80
    fstar: add RewriteCodeGen.fst - Meta-F* tactic for programmatic C++ extraction copilot-swe-agent[bot] 2026-04-05 02:38:29 +00:00
  • e6e878a98a
    fstar: clarify README relationship table heading per review copilot-swe-agent[bot] 2026-04-05 02:01:57 +00:00
  • 1b73e5f1de
    fstar: add fpa_rewriter_rules.h with C++ macros extracted from F* lemmas copilot-swe-agent[bot] 2026-04-05 02:01:12 +00:00
  • 260cf5c357
    Fix LP solver pop invalidation: clear changed bounds on pop, guard mk_value copilot/fix-invalidation-logic copilot-swe-agent[bot] 2026-04-04 20:14:52 +00:00
  • 0cd17f4194
    Initial plan copilot-swe-agent[bot] 2026-04-04 19:47:18 +00:00
  • 8298ba6011 Quick fix for some unsound cases c3 CEisenhofer 2026-04-04 18:36:25 +02:00
  • a58a9114d2 Fix str.< Skolem length generation overhead CEisenhofer 2026-04-04 18:32:02 +02:00
  • a636fb3e83
    Add gc.learned_pop parameter and sat_gc benchmark for push/pop learned clause cleanup copilot/fix-push-pop-scopes-performance copilot-swe-agent[bot] 2026-04-03 20:47:46 +00:00
  • 1218520a6c
    Improve comments in push/pop scope cleanup code copilot-swe-agent[bot] 2026-04-03 18:34:43 +00:00
  • 49e5894592
    Fix push/pop scopes affecting performance of subsequent proofs copilot-swe-agent[bot] 2026-04-03 18:33:53 +00:00
  • 653c49ac5e
    fstar: address review comments - improve comments and table header clarity copilot-swe-agent[bot] 2026-04-03 18:05:55 +00:00
  • e3aa907098
    fstar: formalize FPA rewriter rules from PR #9038 in F* using IEEE 754 axioms copilot-swe-agent[bot] 2026-04-03 18:05:00 +00:00
  • 9b6d87ff89
    Initial plan copilot-swe-agent[bot] 2026-04-03 17:55:25 +00:00
  • b60a44c66b classical Nikolaj Bjorner 2026-04-03 10:33:28 -07:00
  • cdccd389e9 revert s_unknown Nikolaj Bjorner 2026-04-03 10:04:13 -07:00
  • 95dc44b409 bugfix, better debug display of failure Nikolaj Bjorner 2026-04-02 15:51:15 -07:00
  • fa89910452
    Add SASSERT invariants and pre/postconditions to Nielsen seq solver (#9216) Copilot 2026-04-02 21:09:23 -07:00
  • bbb704e63c
    seq_axioms: eliminate redundant mk_literal call in add_clause (#9215) Copilot 2026-04-02 21:08:16 -07:00
  • a4cfbfa274
    Add clarifying comment to m_str_eq.empty() postcondition copilot-swe-agent[bot] 2026-04-03 02:12:35 +00:00
  • 0726edcd0a
    Add SASSERT invariants and pre/postconditions to Nielsen seq solver copilot-swe-agent[bot] 2026-04-03 02:11:02 +00:00
  • 4a5ef833f2
    Initial plan copilot-swe-agent[bot] 2026-04-03 01:41:00 +00:00
  • 378097b5ff
    fix: use already-computed literal in seq_axioms::add_clause copilot-swe-agent[bot] 2026-04-03 01:40:49 +00:00
  • ea09915f89
    Initial plan copilot-swe-agent[bot] 2026-04-03 01:39:57 +00:00
  • ddd8bf84d7
    Replace apply_regex_unit_split with apply_regex_if_split (#9210) Copilot 2026-04-02 14:27:06 -07:00
  • 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) Nikolaj Bjorner 2026-04-02 12:51:47 -07:00
  • a67597d03a
    Replace apply_regex_unit_split with apply_regex_if_split copilot-swe-agent[bot] 2026-04-02 19:31:41 +00:00
  • 3629cd9447 regression fixes Nikolaj Bjorner 2026-04-02 11:42:50 -07:00
  • 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