Default branch

master 8a146a92ec · fix: replace UNREACHABLE with VERIFY for non-COI constraint/monic violations in nra_solver · Updated 2026-03-06 18:54:34 +00:00

Branches

c3 756673f104 · Trying to port integer constraints · Updated 2026-03-06 13:01:21 +00:00	41 94
copilot/add-gcd-algorithms-multivariate-polynomials 04f57f9a03 · Fix GCDheu: use L∞ norm for xi, skip univariate, add bit-size safety limit · Updated 2026-03-06 05:57:53 +00:00	5 4
copilot/remove-unreachable-return-statement-again 870ba21b84 · Remove unreachable return false in match_ubv2s1 · Updated 2026-03-05 17:58:13 +00:00	41 85
copilot/simplify-code-structure 3c8f2c7d9e · Changes before error encountered · Updated 2026-03-05 17:35:44 +00:00	11 2
copilot/remove-unreachable-return-statement c69340596c · Remove unreachable return false in match_ubv2s1 · Updated 2026-03-05 17:25:33 +00:00	11 2
bnsat e62d4e9d50 · Gate early bounded_nlsat on real monomials, remove parameter · Updated 2026-03-05 00:47:29 +00:00	13 3
copilot/fix-re-concat-loop-nullability 9882bf0205 · Add sgraph/seq_plugin + fix re.concat classification and loop nullability · Updated 2026-03-03 03:50:39 +00:00	13 2
copilot/fix-zipt-code-review-improvements 008ef90d4d · Implement ZIPT code review improvements: add euf_sgraph/seq_plugin files and apply 3 fixes · Updated 2026-03-03 03:41:13 +00:00	13 2
copilot/add-unit-test-for-leaks c4e5b79b48 · Add C API unit test for user propagator mk_fresh callback and memory leak detection · Updated 2026-03-03 02:00:13 +00:00	16 2
clemens 6339623877 · Merge pull request #8807 from Z3Prover/copilot/update-clemens-work · Updated 2026-03-02 00:02:53 +00:00	54 17
copilot/update-neq-nielson-implementation 5f92d3344d · Define eq_ref and eq_refs types in ast.h and use them in nseq_ne · Updated 2026-03-01 02:35:32 +00:00	54 10
copilot/sub-pr-8808-again cc5e5e062b · Fix soundness bug: guard mod rewrite with ite when modulus is symbolic or zero · Updated 2026-02-28 22:51:58 +00:00	44 3
copilot/sub-pr-8808 a05520f261 · Guard mod rewrite rule for y=0: skip when concrete zero, use ite for symbolic y · Updated 2026-02-28 22:36:34 +00:00	44 3
copilot/add-abstract-machine-evaluator a4ccb6390d · Integrate rw_table into th_rewriter_cfg and expand populate_rules() · Updated 2026-02-27 04:36:28 +00:00	60 3
copilot/fix-z3-regression-unknown-to-sat 9e96ee91dc · Fix regression: use setup_solver_terms() instead of setup_solver_poly() in nra_solver check() · Updated 2026-02-24 05:11:31 +00:00	144 2
copilot/fix-invalid-model-generation f0612ab7e0 · Initial plan · Updated 2026-02-24 04:44:45 +00:00	144 1
subpave c4c4d18da3 · second round of copilot prompting · Updated 2026-02-23 21:34:06 +00:00	171 2
copilot/fix-invalid-model-proof-generation 6b12bffd55 · Initial plan · Updated 2026-02-23 04:05:35 +00:00	159 1
copilot/fix-tagged-pointer-bug e6607df831 · fixes · Updated 2026-02-17 15:41:07 +00:00	1115 41
copilot/fix-undeclared-identifier-p 768bcb6331 · Initial plan · Updated 2026-02-12 15:02:38 +00:00	1220 1