3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00

Default branch

1b39b0e50f · Fix SIGSEGV in nlsat from incorrect algebraic number comparison (#10129) · Updated 2026-07-15 00:08:08 +00:00

Branches

43ab391dbe · Initial plan · Updated 2026-07-14 15:32:56 +00:00

13
1

1faba5c769 · Fix missing std headers in singlethread WASM wrapper · Updated 2026-07-13 16:32:34 +00:00

26
4

34964402b4 · bugfix about child threads setting force_enable=false for parallel · Updated 2026-07-13 05:07:05 +00:00

353
4

dc8fcb93a6 · Enable macro-finder fallback for auto_config=false mbqi=false · Updated 2026-07-13 04:59:52 +00:00

24
2

50455f9b6d · Delete z3.log · Updated 2026-07-13 01:29:16 +00:00

37
3

9b8bfe6a26 · smt: restore direct quantifier internalization in theory::mk_literal · Updated 2026-07-12 08:29:30 +00:00

39
1

be243ba2bd · refactor: address code review feedback for transcendental decimal formatting · Updated 2026-07-12 02:19:37 +00:00

43
3

33d260a9c3 · Fix assertion violation in spacer_qe_project.cpp when model evaluation doesn't produce a numeral · Updated 2026-07-12 01:57:59 +00:00

43
2

4c7e421514 · Refactoring · Updated 2026-07-11 20:29:43 +00:00

100
576

e83e8f695a · Fix array lambda final-check livelock (snapshot-regression iss-6364) · Updated 2026-07-11 07:02:45 +00:00

44
1

984dbb3926 · Clean up std::to_string(1) literal in array_decl_plugin.cpp · Updated 2026-07-10 22:11:41 +00:00

46
3

37f1ac2e5d · Fix MBQI model-construction regression on UFLIA (iss-5421) · Updated 2026-07-10 07:56:41 +00:00

48
1

b1dc9c0ef2 · Fix OOB bounds-checking in smt_model_finder.cpp to prevent segfaults · Updated 2026-07-09 16:43:47 +00:00

50
2

c0e49d6979 · Fix Z3 infinite loop: change bv_sort_ac default from false to true · Updated 2026-07-09 16:18:50 +00:00

50
2

f37be0ec64 · Increase Ubuntu OCaml regression timeout in CI · Updated 2026-07-09 01:59:46 +00:00

54
2

f92a0e2d46 · Fix FP E-matching regression: remove redundant m_new_def from theory_lra::can_propagate_core() · Updated 2026-07-07 20:57:47 +00:00

59
2

6610545c08 · disable loop split set · Updated 2026-07-05 19:03:27 +00:00

101
21

a0da774400 · lp: gate per-row batched fixed-column explanation behind lp.batch_explain_fixed_in_row · Updated 2026-07-05 18:35:29 +00:00

96
2

85467986ad · seq_monadic: whole-language monadic decomposition for regex membership (log-only diagnostic) · Updated 2026-07-05 12:28:34 +00:00

100
577

380ad825e6 · lp: restore deterministic integer heuristic gates by default (random_hammers=false) · Updated 2026-07-05 08:49:29 +00:00

78
1