mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 23:25:36 +00:00
Code Activity
z3/src
History
Exact
github-actions[bot] 7ea6e9bed4
simplify parallel_tactical2: use std::min and consistent mk_not 
- Replace manual conflict cap with std::min in update_max_conflicts()
- Use mk_not(m, c) instead of mk_not(expr_ref(c, m)) for consistency
  with the existing call pattern at line 349

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-05-14 05:35:11 +00:00
..
ackermannization Fix off-by-one vulnerabilities: use range-based for on goals; cache loop bound 2026-02-19 22:37:22 +00:00
api Go bindings: extract CGo slice-conversion helpers to eliminate boilerplate (#9465) 2026-05-06 12:32:53 -07:00
ast Silence GCC false positives in bound propagation and mpz sign-cell paths (#9530) 2026-05-13 17:24:13 -04:00
cmd_context fixes to tptp front-end 2026-05-13 14:56:34 -07:00
math nla_grobner: remove dead code and fix indentation (#9423) 2026-04-29 11:12:45 -07:00
model Remove redundant default constructors when they're the only constructor (#8461) 2026-02-18 20:58:01 -08:00
muz Refactor sls_euf_plugin.cpp validate_model and add SASSERT in udoc_relation.cpp 2026-03-09 16:57:59 +00:00
nlsat making try-for tactic exception resilient on cancelation 2026-04-26 15:58:24 -07:00
opt fix box mode: reset bounds before each objective 2026-03-19 17:07:21 -10:00
params Simplify parallel SMT code: clean comments and deduplicate stat computation (#9507) 2026-05-12 14:41:20 -04:00
parsers Revert "Refactor find_psort_decl() to return std::optional<psort_decl*> (#8339)" 2026-02-18 20:57:56 -08:00
qe Simplify extract_var_bound via operator normalization (#9062) 2026-03-22 16:01:12 -07:00
sat connect parallel tactical2 as side load 2026-05-13 14:59:05 -07:00
shell Integrate TPTP with internal APIs via cmd_context, add embedded-string TPTP regression tests, and fix TFF arithmetic/timeout regressions (#9483) 2026-05-12 19:29:58 -04:00
smt connect parallel tactical2 as side load 2026-05-13 14:59:05 -07:00
solver simplify parallel_tactical2: use std::min and consistent mk_not 2026-05-14 05:35:11 +00:00
tactic Throttle lia2card in QF_LIA preamble (mk_preamble_tactic) (#9489) 2026-05-11 12:03:09 -04:00
test TPTP frontend: enforce implicit universal quantification for free variables and add regression coverage (#9527) 2026-05-13 13:19:14 -04:00
util Silence GCC false positives in bound propagation and mpz sign-cell paths (#9530) 2026-05-13 17:24:13 -04:00
CMakeLists.txt git bindings v1.0 2026-02-18 21:02:25 -08:00