3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-24 19:06:21 +00:00

Default branch

459629c662 · bugfixes to ho_matcher · Updated 2026-05-24 01:06:04 +00:00

Branches

314ffe6c29 · nla_grobner: remove dead code and fix indentation · Updated 2026-04-28 21:09:31 +00:00

61
1

8bbac04a26 · Refactor: extract saturating_add helper, simplify hash-check condition · Updated 2026-04-28 16:12:33 +00:00

139
428

07a02de93f · Apply ZIPT code review improvements to euf_seq_plugin/euf_sgraph · Updated 2026-04-24 23:07:47 +00:00

73
2

a23d2b7884 · simplify: replace custom reset_unsafe RAII struct with on_scope_exit · Updated 2026-04-24 21:07:11 +00:00

73
1

168b63b44a · Fix loop merging to use a->get_arg(0) consistently for body enode and expression · Updated 2026-04-24 01:59:48 +00:00

73
3

e503ead008 · Address review feedback for qe-lite BV case split changes · Updated 2026-04-21 20:37:53 +00:00

83
3

e10109443b · Simplify backbone/parallel code from PR #9343 · Updated 2026-04-20 21:05:12 +00:00

85
1

772ee91cbf · Initial plan · Updated 2026-04-19 14:54:51 +00:00

86
1

e050781a11 · refactor(go): extract exprsToApps helper to eliminate duplication in QE projection functions · Updated 2026-04-13 21:35:32 +00:00

94
1

717888572a · simplify solve_eqs: move early return, replace ternary with if, fix indentation · Updated 2026-04-12 21:01:41 +00:00

96
1

23ae00a57e · update count to 2 · Updated 2026-04-09 23:39:51 +00:00

108
0
Included

f2f1d69204 · Initial plan · Updated 2026-04-09 09:03:21 +00:00

113
1

2e9e88fe44 · Initial plan · Updated 2026-04-09 09:02:20 +00:00

113
1

c49b403922 · fstar: address code review comments - document gen_rhs_expr_list and strip-components · Updated 2026-04-06 01:51:11 +00:00

117
9

260cf5c357 · Fix LP solver pop invalidation: clear changed bounds on pop, guard mk_value · Updated 2026-04-04 20:14:52 +00:00

117
2

a636fb3e83 · Add gc.learned_pop parameter and sat_gc benchmark for push/pop learned clause cleanup · Updated 2026-04-03 20:47:46 +00:00

117
4

8d7ed66ebf · Fix Specbot Crash Analyzer: move Z3 build to pre-steps to avoid MCP session timeout (#9200) · Updated 2026-04-02 15:48:25 +00:00

117
0
Included

40485e69be · Simplify extract_var_bound via operator normalization (#9062) · Updated 2026-03-22 23:01:12 +00:00

155
0
Included

bb1c8ab230 · Fix ostrich workflow OOM kill: use ninja -j1 to limit compilation memory (#9068) · Updated 2026-03-20 21:17:31 +00:00

163
0
Included

a37003fa2d · fix #8185: add FPA rewriter simplifications for fma with zero multiplicand and classification of int-to-float conversions · Updated 2026-03-18 17:30:55 +00:00

181
1