SRI-CSL / yices2 / 25536263059

67%

master: 71%

Build Type

push

github

Committed by disteph

Commit Message

mcsat: gate preprocessor diag prints on YICES_PP_TRACE; trim windows CI

Two fixes / aids for the windows-latest|release|--enable-thread-safety
--enable-mcsat mcsat_tuples failure investigation:

1. Gate every preprocessor.c TEMP DIAG stderr print behind an env var
   YICES_PP_TRACE. The existing prints were unconditional, so they
   leaked into the regression-test stderr stream and broke ~21 mcsat
   regression tests (`make test`) that diff stderr against expected
   output. With the gate, the prints are silent unless the env var is
   set, so:

     - `make test` regressions are clean again on every CI config
     - the prints are still available when needed: set
       YICES_PP_TRACE=1 (any non-empty / non-"0" value) before running
       the failing binary.

   Implementation: a tiny static helper `pp_diag_enabled()` reads the
   env var once (cached in a static int -- benign one-time race under
   --enable-thread-safety), and a `PP_DIAG(...)` macro wraps
   fprintf(stderr,...)+fflush(stderr). All call sites switched in
   build_value_from_flat, preprocessor_build_tuple_model, and
   preprocessor_build_model.

   Verified locally:
     mcsat_tuples                          -> 0   "[pp_build|build_value" lines
     YICES_PP_TRACE=1 mcsat_tuples         -> 631 "[pp_build|build_value" lines

2. Trim Windows CI to only the failing config and only the API tests
   so each iteration takes ~10 minutes instead of an hour:

     - Matrix: mode=[release], config-opt=[--enable-thread-safety
       --enable-mcsat] (was 2x3=6 jobs, now 1).
     - Test step: just `make check-api` with YICES_PP_TRACE=1
       exported, so mcsat_tuples emits the full preprocessor trace.
       The `make test` regression sweep is dropped for now.

   Both changes are TEMP and clearly commented; the original matrix
   and test step are restored at the end of this debugging session.

Coverage Stats

43 of 49 new or added lines in 1 file covered. (87.76%)

76 existing lines in 1 file now uncovered.

84692 of 126242 relevant lines covered (67.09%)

1633053.41 hits per line