26675300141
69%
master: 71%

Ran 30 May 2026 05:18AM UTC

Jobs 1

Files 486

Run time 2min

Badge

Embed ▾

Committed 29 May 2026 08:46PM UTC coverage: 68.798% (+3.4%) from 65.375%

Build # 26675300141

Build Type

push

github

Committed by

ahmed-irfan

Commit Message

Rework clause-deletion heuristic to CaDiCaL-style schedule

Replace the geometric, learned-clause-count-triggered reduce schedule
with a CaDiCaL-style one: trigger on conflict count and rebase the
reduction bound to num_conflicts + r-interval * sqrt(num_conflicts).

- context_solver.c: factor the reduce step into try_reduce_heuristic();
  trigger on num_conflicts instead of num_learned_clauses; widen the
  running reduce_threshold to uint64_t (conflict count is unbounded).
- search_parameters: drop r-threshold/r-fraction/r-factor, add
  r-initial-threshold and r-interval (defaults 300 / 25, matching
  CaDiCaL's reduceinit / reduceint).
- Update doc/YICES-LANGUAGE, doc/sphinx parameters table, and the
  interactive (help ...) entries for the renamed parameters.

Coverage Stats

10 of 10 new or added lines in 1 file covered. (100.0%)

8005 existing lines in 44 files now uncovered.

87475 of 127148 relevant lines covered (68.8%)

1646632.75 hits per line

Coverage Regressions

Lines	Coverage	∆	File
1980	48.71	22.35%	src/api/yices_api.c
1499	35.73	35.73%	src/solvers/cdcl/new_sat_solver.c
920	52.45	2.15%	src/frontend/smt2/smt2_commands.c
532	15.75	1.03%	src/io/term_printer.c
383	81.43	0.18%	src/context/context.c
352	68.58	4.42%	src/model/concrete_values.c
319	81.73	-10.28%	src/mcsat/preprocessor.c
274	79.39	0.59%	src/mcsat/solver.c
225	81.56	1.14%	src/solvers/cdcl/smt_core.c
193	78.2	9.1%	src/context/context_solver.c
167	55.24	55.24%	src/solvers/cdcl/delegate.c
152	25.0	23.46%	src/api/search_parameters.c
152	72.84	-0.08%	src/mcsat/eq/equality_graph.c
150	37.32	3.05%	src/frontend/yices_smt2.c
99	0.0	0.0%	src/mcsat/tracing.c
67	36.86	26.03%	src/io/concrete_value_printer.c
64	64.76	0.37%	src/mcsat/conflict.c
54	54.2	46.34%	src/api/context_config.c
49	81.4	0.72%	src/terms/term_manager.c
45	78.53	-0.09%	src/exists_forall/efsolver.c
44	87.97	2.45%	src/frontend/smt2/smt2_printer.c
37	91.35	0.08%	src/mcsat/bool/bool_plugin.c
32	91.54	3.69%	src/mcsat/uf/uf_plugin.c
32	65.67	-1.52%	src/model/val_to_term.c
31	50.44	0.0%	src/frontend/common/parameters.c
28	61.65	0.0%	src/mcsat/bv/bv_explainer.c
24	2.48	2.48%	src/api/yices_error.c
19	50.22	-1.02%	src/io/yices_pp.c
16	90.42	0.16%	src/terms/terms.c
16	50.0	17.69%	src/utils/string_utils.c
12	80.65	1.02%	src/terms/term_utils.c
8	81.15	0.0%	src/utils/string_buffers.c
6	81.79	-1.09%	src/mcsat/bv/bv_evaluator.c
4	96.1	0.02%	src/mcsat/bool/cnf.c
3	87.95	3.27%	src/mcsat/trail.c
3	92.0	8.44%	src/model/concrete_values.h
2	86.4	-0.34%	src/mcsat/bv/bv_bdd_manager.c
2	61.17	-0.22%	src/mcsat/bv/explain/arith.c
2	96.77	-0.72%	src/mcsat/bv/explain/arith_utils.c
2	70.91	3.33%	src/mcsat/value.c
2	89.04	-1.37%	src/solvers/bv/bv64_intervals.c
2	77.78	77.78%	src/solvers/cdcl/new_sat_solver.h
1	89.14	-0.03%	src/solvers/simplex/simplex.c
1	58.79	17.97%	src/terms/types.c

Jobs

ID	Job ID	Ran	Files	Coverage
1	26675300141.1	30 May 2026 05:17AM UTC	486	68.8	GitHub Action Run

SRI-CSL / yices2 / 26675300141
69%
master: 71%

README BADGES
x

Markdown

Textile

RDoc

HTML

Rst

Coverage Regressions

Jobs

Source Files on build 26675300141

SRI-CSL / yices2 / 26675300141 69% master: 71%

README BADGES x

Markdown

Textile

RDoc

HTML

Rst

Coverage Regressions

Jobs

Source Files on build 26675300141

SRI-CSL / yices2 / 26675300141
69%
master: 71%

README BADGES
x