3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 01:49:03 +00:00

Default branch

3879e2190a · recompile workflows · Updated 2026-04-01 16:27:45 +00:00

Branches

c3

6e8c201234 · fix test · Updated 2026-04-01 23:00:01 +00:00

20
331

008a101c08 · seq_eq_solver: add pointer-equality fast path in has_len_offset and use all_of in find_branch_candidate · Updated 2026-04-01 22:08:19 +00:00

0
2

ec495c094c · seq_ne_solver: short-circuit propagate_ne2eq for str.unit elements · Updated 2026-04-01 22:06:52 +00:00

0
2

4f5c19acfa · remove unused functions from seq_nielsen · Updated 2026-04-01 17:16:12 +00:00

20
320

367ae39a50 · fix CI: add set_lower/upper_int_bound to nielsen_node, fix nseq_basic simplify_and_init call · Updated 2026-03-31 21:05:44 +00:00

20
317

749f161302 · feat: add Z3_mk_type_variable to .NET, TypeScript, and C++ bindings · Updated 2026-03-31 00:45:18 +00:00

11
1

c1112d430f · Remove old tactic class, use simplifier-backed mk_bv_size_reduction_tactic · Updated 2026-03-30 03:43:03 +00:00

19
3

8904fdaaf8 · Convert nnf/snf tactics to dependent_expr_state_tactic with nnf_simplifier · Updated 2026-03-28 22:33:38 +00:00

19
2

541b2294fe · Convert normalize-bounds tactic to a dependent_expr_simplifier · Updated 2026-03-28 22:30:26 +00:00

19
2

21590144f7 · Have theory_nseq use not_contains_axiom instead of unroll_not_contains · Updated 2026-03-23 04:55:58 +00:00

217
267

4dc705d932 · seq_nielsen: handle unit(A) = unit(B) ++ rest equations deterministically · Updated 2026-03-23 00:08:08 +00:00

217
262

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

36
0
Included

3c1b1da8ac · Fix three nseq quick-win issues: non-greedy quantifiers, bool-eq normalization, stuck-node crash, precheck SAT soundness · Updated 2026-03-21 03:04:00 +00:00

217
254

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

44
0
Included

aef0c14a35 · Fix nseq divergence: classify Skolem terms as s_var, fix at_axiom, remove UNREACHABLE, add stall detection, filter opaque equations, handle mk_seq_eq assignments · Updated 2026-03-20 17:22:01 +00:00

217
249

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

62
1

23b7e109bd · partial updates to test · Updated 2026-03-18 17:04:07 +00:00

217
218

c41753baad · Initial plan · Updated 2026-03-18 00:09:12 +00:00

65
1

d3f5fd6825 · Fix Java UnsatisfiedLinkError on macOS (#7640) · Updated 2026-03-17 23:59:37 +00:00

65
1

027a4b8be3 · Initial plan · Updated 2026-03-17 16:49:37 +00:00

67
1