Default branch

master f34baf1ff4 · QF_NRA: avoid degree-80 perfect-square factoring blowup by raising default prime trials (#10506) · Updated 2026-08-14 20:42:05 +00:00

Branches

nla-squeeze-nlsat-backoff 0bb2502469 · nla: add a lemma-loop circuit breaker to the eager bound squeeze · Updated 2026-08-14 23:37:27 +00:00	1 2
seq-monadic-orientation 8c8fa2a7b6 · Let the monadic regex solver choose the direction it reads memberships in · Updated 2026-08-14 21:34:17 +00:00	0 3
copilot/solution-soundness-bug-fix 4191d2db44 · Fix unsound sat for str.to_re of a unit-length str.substr · Updated 2026-08-14 16:32:47 +00:00	4 2
copilot/fix-unsat-bug-case-split 78ea1c0aa5 · Clarify divisibility equality guard · Updated 2026-08-14 16:06:52 +00:00	4 6
copilot/fix-unsat-bug-sat-euf-true 0d57e796b4 · Clarify comments on clamped cardinality bounds · Updated 2026-08-14 16:04:34 +00:00	4 3
c3 599cd08f8b · Let's try to use the view operator for seq_monadic; that will be interesting... · Updated 2026-08-14 03:28:46 +00:00	22 647
rrmerge ad8bfcf00b · Only cache an l_true nlsat verdict in the final check · Updated 2026-08-13 14:42:23 +00:00	22 25
fix-10385 00dee3253a · Fix parent generation cache replay · Updated 2026-08-13 12:13:44 +00:00	12 1
seq-monadic-sl 4842fa5aad · split equalities on bag alignment · Updated 2026-08-12 03:41:54 +00:00	21 0	Included
nla-avoid-grobner-horner 27bed6fac4 · Cap the mod-congruence rule and key the eager bounds pass on the live ladder · Updated 2026-08-12 02:24:37 +00:00	22 15
c3-reverted-dnf-opt ef5f9f22c3 · Try reverting seq-dnf-opt in c3 · Updated 2026-08-12 01:21:28 +00:00	22 647
seq-filter-single-var-groups 84645d0ca1 · seq_monadic: single-variable emptiness pre-filter with focused core · Updated 2026-08-11 20:02:20 +00:00	22 1
arith-round-robin2 62029c91f5 · Split nla_core::check into cheap and expensive phases · Updated 2026-08-11 17:32:20 +00:00	37 10
arith-round-robin 4210f3ec5d · Update monomial_bounds.cpp · Updated 2026-08-10 16:42:32 +00:00	37 10
seq-dnf-opt 16ffa89dc5 · Merge remote-tracking branch 'origin/seq-monadic-sl' into seq-dnf-opt · Updated 2026-08-10 10:53:08 +00:00	33 12
seq-monidic-core 585d7e328d · seq_monadic: track unsat core inline during search, drop deletion-based minimization · Updated 2026-08-10 00:15:10 +00:00	25 1
copilot/fix-assertion-violation-z3-solver-bug 86663abb4e · Merge master into assertion violation fix · Updated 2026-08-09 23:58:07 +00:00	24 4
seq-length-lookahead 70b2a69559 · Fix min_length calculation using max_length · Updated 2026-08-09 19:23:08 +00:00	30 8
c3-budget cf47297594 · Recalibrate the seq_monadic work budget for the interval-refinement product · Updated 2026-08-08 20:08:51 +00:00	33 635
seq-monadic-budget a9894be876 · Recalibrate the seq_monadic work budget for the interval-refinement product · Updated 2026-08-08 19:59:04 +00:00	33 1