SRI-CSL / yices2 / 26473630241

69%

master: 69%

Build Type

Pull #630

github

Committed by disteph

Commit Message

Wide projection: address second review pass

Two cleanup items raised by review:

1. tests/api/test_generalize_model.c: remove the unused helper
   run_both_modes_quiet. It was a leftover from an earlier iteration
   that printed less per-test detail; every caller now uses
   run_both_modes. Triggered -Wunused-function and contradicted the
   "builds clean" claim.

2. src/model/generalization.h: a second variant block (the gen_model_*
   enumeration) still called gen_model_by_projection "the new default
   for the public API". The mode is opt-in via YICES_GEN_BY_PROJ_WIDE;
   YICES_GEN_BY_PROJ and YICES_GEN_DEFAULT keep the legacy path. An
   earlier commit fixed the short variant block (line 39) but missed
   this one.

The reviewer's open question about "SAT-guided enumeration is the
default" in the checklist is already fixed: the checklist was rewritten
in the recent PR-description trim and no longer contains that claim.

Builds clean in MODE=release and MODE=debug. check-api: 36/36 pass.

Pull Request Pull Request #630: Add wide (truth-invariant) model generalization mode

Coverage Stats

411 of 533 new or added lines in 2 files covered. (77.11%)

221 existing lines in 2 files now uncovered.

88091 of 127684 relevant lines covered (68.99%)

1614710.65 hits per line